Journal: D-INFK Technical Report

Abbreviation

Publisher

ETH Zurich, Department of Computer Science

Journal Volumes

ISSN

Description

Filters

Reset filters

Search Results

Publications 1 - 10 of 647
  • Automatic Inference of Heap Properties Exploiting Value Domains
    Item type: Report
    Ferrara, Pietro; Müller, Peter; Nováček, Miloš (2013)
    D-INFK Technical Report
    Effective static analysis of heap manipulating programs is required to track precise information about the heap structures and values computed by the program. In this paper, we introduce a combined heap and value analysis that infers complex invariants for recursive data structures like lists and trees, in particular relations between value fields of heap-allocated objects. Our analysis does not require any manual annotation of the program. Different performance/precision ratios are achieved by selecting different value domains. The analysis has been implemented in the generic static analyzer Sample. The experimental results show that the analysis infers invariants automatically that required manual annotations in the state-of-the-art analyses.
  • On the advice complexity of the set cover problem
    Item type: Report
    Komm, Dennis; Královič, Richard; Mömke, Tobias (2011)
    D-INFK Technical Report
    Recently, a new approach to get a deeper understanding of online computation has been introduced: the study of the advice complexity of online problems. The idea is to measure the information that online algorithms need to be supplied with to compute high-quality solutions and to overcome the drawback of not knowing future input requests. This concept was successfully applied to many prominent online problems including paging, the k-server problem, metrical task systems, or job shop scheduling. In this paper, we study the advice complexity of an online version of the well-known set cover problem introduced by Alon et al.: for a ground set of size n and a set family of m subsets of the ground set, we obtain bounds in both n and m. We prove that n bits of advice are both sucient and necessary to perform optimally. Furthermore, for any constant c, we prove that n
  • Experiments in computer system design
    Item type: Report
    Wirth, Niklaus (2010)
    D-INFK Technical Report
  • Scyther: Unbounded verification of security protocols
    Item type: Report
    Cremers, C.J.F. (2011)
    D-INFK Technical Report
    We present a new cryptographic protocol verification tool called Scyther. The tool is stateof- the-art in terms of verification speed and provides a number of novel features. (1) It can verify most protocols for an unbounded number of sessions in less than a second. Because no approximation methods are used, all attacks found are actual attacks on the model. (2) In cases where unbounded correctness cannot be determined, the algorithm functions as a classical bounded verification tool, and yields results for a bounded number of sessions. (3) Scyther can give a “complete characterization” of protocol roles, allowing protocol designers to spot unexpected possible behaviours early. (4) Contrary to most other verification tools, the user is not required to provide so-called scenarios for property verification, as all possible protocol behaviours are explored by default. The algorithm expands on ideas from the Athena algorithm. We describe the algorithm, choice of heuristics, and discuss experimental results. The tool has been used already successfully for research as well as teaching of security protocol analysis.
  • An On-the-fly model-checker for security protocol analysis
    Item type: Report
    Basin, David; Mödersheim, Sebastian; Viganò, Luca (2003)
    D-INFK Technical Report
    We introduce the on-the-fly model-checker OFMC, a tool that combines two ideas for analyzing security protocols based on lazy, demand-driven search. The first is the use of lazy data-types as a simple way of building efficient on-the-fly model checkers for protocols with infinite state spaces. The second is the integration of symbolic techniques and optimizations for modeling a lazy Dolev-Yao intruder, whose actions are generated in a demand-driven way. We present both techniques, along with optimizations and proofs of correctness and completeness. Our tool is state-of-the-art both in terms of coverage and performance. For example, it finds all (but one) known attacks and discovers a new one in a test-suite of 36 protocols from the Clark/Jacob library in under one minute of CPU time for the entire suite. We also give examples demonstrating how our tool scales to, and finds errors in, large industrial-strength protocols.
  • Write - An extensible text editor for the Oberon system
    Item type: Report
    Szyperski, Clemens A. (1991)
    D-INFK Technical Report
  • Oberon as an implementation language for COM objects
    Item type: Report
    Gutknecht, Jürg (1999)
    D-INFK Technical Report
    This is a short report on a short project, carried out during a 3-month sabbatical stay at Microsoft Research in the fall of 1998. The motivation for this endeavor was doublefold: (a) verify the degree of language independence of the COM component technology and (b) explore COM as a potential commercial environment and framework for Oberon applications. The project finally converged towards a simple case study, an electronic accounting system implemented in Oberon as a COM server under Windows NT and illustratively used by a Visual Basic client.
  • Certified dense linear system solving
    Item type: Report
    Mulders, Thom; Storjohann, Arne (2000)
    D-INFK Technical Report
    The following problems related to linear systems are studied: finding a diophantine solution; finding a rational solution; proving no diophantine solution exists; proving no rational solution exists. These problems are reduced, via randomization, to that of computing an expected constant number of rational solutions of square nonsingular systems using adic lifting. The bit complexity of the latter problem is improved by incorporating fast arithmetic and fast matrix multiplication. The resulting randomized algorithm for certified dense linear system solving has substantially better asymptotic complexity than previous algorithms for either rational or diophantine linear system solving.
  • Distributed small connected spanning subgraph: Breaking the diameter bound
    Item type: Report
    Ram, L. Shankar; Vicari, Elias (2011)
    D-INFK Technical Report
Publications 1 - 10 of 647