Vortragsreihe Grundlagen der Informatik
- Leitung: Esparza, Mayr, Nipkow, Scheideler, Seidl
- Zeit und Ort: Donnerstag, 16:00 Uhr, 03.11.018
Verification of Multithreaded Java Programs
Abstract: The reachability problem is undecidable for programs with both recursive procedures and multiple threads communicating through shared memory. Attempts to overcome this problem have been the focus of much recent research. One approach is to use context-bounded reachability, i.e. to consider only those runs in which the active thread changes at most k times, where k is fixed. However, to the best of our knowledge, context-bounded reachability has not been implemented in any tool so far, primarily because its worst-case runtime is prohibitively high, i.e. O(n^k), where n is the size of the shared memory. Moreover, existing algorithms for context-bounded reachability do not Admit a meaningful symbolic implementation (e.g., using BDDs) to reduce the run-time in practice. In this talk, we propose an improvement that overcomes this problem. We also demonstrate the tool jMoped, a user-friendly test environment for Java programs, and report on experiments of our approach.
An abstract domain for reasoning about field access and array indexing
Abstract: My talk is about our pursuit of methods to reason about field and array access in safety critical code. We need this, for example, when trying to check for race conditions in Posix Threaded C, which was the topic of my master thesis. To reason about situations when the mutexes in one array protect the data in another or when we have an array of structs with a per-element locking discipline, we present an abstract domain for must-equalities between addresses.
This domain is a "smooth" combination of Herbrand and affine equalities, which enables us to describe field accesses and array indexing, respectively. While the full combination of uninterpreted functions with affine equalities results in intractable assertion checking algorithms, our modest approach allows us to construct an inter-procedural analysis of address must-equalities that runs in polynomial time. Having described our address analysis, I will then turn back to how we can use this to infer affine relationships between locks and the data they are supposed to protect.
SPREAD: An Adaptive Scheme for Redundant and Fair Storage in Dynamic Heterogeneous Storage Systems
Abstract: We consider the problem of designing an adaptive hash table for redundant data storage in a system of storage devices with arbitrary capacities. Ideally, such a hash table should make sure that (a) a storage device with x% of the available capacity should get x% of the data, (b) the copies of each data item are distributed among the storage devices so that no two copies are stored at the same device, and (c) only a near-minimum amount of data replacements is necessary to preserve (a) and (b) under any change in the system. Hash tables satisfying (a) and (c) are already known, and it is not difficult to construct hash tables satisfying (a) and (b). However, no hash table was known before that can satisfy all three properties as long as this is in principle possible. We present a strategy that solves this problem for the first time. As long as (a) and (b) can in principle be satisfied, our scheme preserves (a) for every storage device within a (1 ± epsilon) factor, with high probability, where epsilon > 0 can be made arbitrarily small, guarantees (b) for every data item, and only needs a constant factor more data replacements than minimum possible in order to preserve (a) and (b).
Type-Checking Twoway Tree Transducers
Abstract: Tree walking transducers have been shown to be an expressive formalism for reasoning about XSLT-like document transformations. A type in XML is a finite-state specification of a set of legal documents. Type-checking a transformation means to verify that all documents adhering to the input type are necessarily transformed into documents from the given output type. Exact type checking is decidable for finite-state tree transducers, but can be extremely expensive. Here we are concerned with characterizations of cases where type-checking can be performed in polynomial time. Our approach uses forward inference: given a transducer and input type, we determine the corresponding output language. In general, this output language is not a type, i.e., is not regular. However, its intersection emptiness with a given type can be decided. Using this approach, we exhibit that type-checking is polynomial --- given that the output type is specified by a bottom-up deterministic tree automaton or, alternatively, a top-down deterministic tree automaton, and that every input node is visited by the transducer only a bounded number of times. Subsequently, we extend these methods to tree walking transducers with call-by-value parameters. There, the complexity also depends on the number of parameters.
A Toolchain for Verifying C Programs
Abstract: VCC is a C compiler and verification system still under development. It promises to automatically verify a suitably annotated C program. Currently, this system is used in a substantial verification task to proof the correctness of the Microsoft hypervisor. In practice, however, the system showed several shortcomings centered around the annotation of a programs, i.e. finding necessary invariants and tweaking them such that the automatic tools are able to check them. To tackle these problems, we developed HOL-Boogie, a tool integrated in the described system and building on the interactive theorem prover Isabelle. In this setting, the logical representation of a C program as seen by an automatic prover can be inspected and also verified. Enriched with labels relating parts of the formula to the original program, this logical representation allows to find missing assertions or identify flaws in the specification. We demonstrate this tool and give examples of its usage, in particular hinting to how the above mentioned problems of VCC can be solved.
Approximative Methods for Monotone Systems of Min-Max-Polynomial Equations
Abstract: A monotone system of min-max-polynomial equations (min-max-MSPE) over the variables X_1, ..., X_n has for every i exactly one equation of the form X_i = f_i(X_1, ..., X_n) where each f_i(X_1, ..., X_n) is an expression built up from polynomials with non-negative coefficients, minimum- and maximum-operators. The question of computing least solutions of min-max-MSPEs arises naturally in the analysis of certain stochastic games. Min-max-MSPEs generalize MSPEs for which convergence speed results of Newton's method have been recently established. We present the first two methods for approximatively computing least solutions of min-max-MSPEs which converge at least linearly. Whereas the first one converges faster, a single step of the second method is cheaper.
joint work with Javier Esparza, Thomas Gawlitza and Helmut Seidl
Cryptographic protocols with single blind copying and an XOR operator
Abstract: Modeling interesting fragments of cryptographic protocols using decidable classes of first order logic has been pursued by several researchers. Another direction of work has been to study the verification problem of cryptographic protocols in the presence of algebraic properties of cryptographic operations. We consider cryptographic protocols with the single blind copying restriction, which means that at most one piece of unknown data is copied in each step of the protocol. These protocols can be modeled using the class of Horn clauses called flat and one-variable clauses, and the verification problem is known to be DEXPTIME-complete. In this talk we look at the decidability and complexity issues when an XOR operator is additionally used in the protocols.
Lowest Common Ancestor Algorithms for Dags
Abstract: We consider the problem of computing lowest common ancestors (LCAs) in general directed acyclic graphs. While the problem is fairly understood for the special case of trees, (non-straightforward) generalizations to dags have only be considered in recent years. Since LCAs in dags are not unique, it is distinguished between computing one arbitrary (representative) LCA and computing all LCAs for vertex pairs. In this talk we consider two basic algorithmic techniques that lead to state-of-the-art solutions for LCA problems in dags, namely matrix-multiplication-based approaches and a path cover method. Whereas the currently best upper time bounds rely on the first method, the path cover approach is beneficial in the case that the width of the input dag is restricted. Further, both techniques can be combined to design algorithms that combine the advantages of both approaches, thereby significantly restricting the class of dags for which the worst case upper time bound is actually attained.
Strategy Iteration using Non-Deterministic Strategies for Solving Parity Games
Abstract: Paritätsspiele sind Zwei-Personen-Spiele, welche über einem gerichteten, knotengewichteten Graphen gespielt werden. Jeder Knoten ist dabei genau einem der beiden Spieler zugeordnet. Strategieiteration, d.h., die iterative Verbesserung einer anfänglichen Strategie hin zu einer optimalen, ist dabei ein oft diskutierter Ansatz zur Berechnung der Gewinnmengen der Spieler in einem Paritätsspiel, siehe:
- Jurdzinski/Vöge 2000: A discrete strategy improvement algorithm for solving parity games
- Björklund/Sandberg/Vorobyov 2003: A discrete subexponential algorithm for parity games
- Björklund/Sandberg/Vorobyov 2004: A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games
- Schewe 2007: An optimal strategy improvement algorithm for solving parity games
Reachability in Recursive Markov Decision Processes
Abstract: Markov decision processes are a fundamental model in the area of system design and control optimization. In this talk, I will concentrate on a class of infinite-state Markov decision processes generated by stateless pushdown automata (pBPA). These processes combine non-deterministic and probabilistic choice with recursive calls. The reachability problem for pBPA is as follows: Given a set T of configurations and an initial configuration s, decide whether there is a suitable strategy such that the probability of reaching a configuration of T by a path initiated in s is equal to (or different from) a given rational number. This problem is the most basic one in the area of controller synthesis and verification. The main aim of this talk is to present results on decidability and complexity of the reachability problem for pBPA and to illustrate some methods used for solving this problem. I will start with a discussion of general properties of infinite-state Markov decision processes that are connected with the reachability problem. Then I will present polynomial-time algorithms for the qualitative version of the reachability problem for pBPA. I will conclude with a presentation of open problems and some possibilities for further research. This talk is based on joint work with Vaclav Brozek, Vojtech Forejt, and Antonin Kucera.
A Bit of Social Choice Theory in HOL: Arrow and Gibbard-Satterthwaite
Abstract: In 1950, Kenneth Arrow proved his famous impossibility theorem about voting systems: under certain minimal plausible fairness conditions, the only voting system left is a dictatorship. In 1973, Gibbard and Satterthwaite independently proved a similar result where nonmanipulabiliy forces a dictatorship. These two theorems are closely related staples of social choice theory and numerous proofs for them have been given in the literature. Yet logicians, as usual, have found fault with (some of) these proofs: "The standard and textbook proofs of Arrow's general impossibility theorem are, like the original proofs, invalid." [Routley79]. This was written 30 years ago but is still valid. In this paper I formalize some recently published proofs of Arrow's theorem in HOL and find that in places they still suffer from opaqueness and missing cases. Then I derive Gibbard-Satterthwaite from Arrow; here the standard construction appears to be free of holes.
Locales - a Module System for an Interactive Theorem Prover
Abstract: Locales are a module system for the Isabelle theorem prover. They combine the notion of proof context with techniques from algebraic specification. Locales have been designed to support the formalisation of abstract algebra in Higher-Order Logic but are actively used in other applications as well -- for example, in program verification -- and they are not restricted to the HOL object- logic of Isabelle.
We give an overview of the design of locales, which is driven by supporting the working prover (ie. the user of an interactive prover). Unlike in other module systems, the inheritance relation between modules is not fixed. This reflects that relations between algebraic structures may be discovered after their declaration. We distinguish import dependencies from interpretation dependencies. The latter reflect post-facto extensions of the inhertance relation and must be justified by proofs.