CAV on Sunday, July 18th

09:00‑10:00 Invited Talk
Chair: Vineet Kahlon
Location: AT LT4
09:00 Somesh Jha
Retrofitting Legacy Code for Security
10:30‑12:30 Synthesis
Chair: Kedar Namjoshi
Location: AT LT4
10:30 Rüdiger Ehlers
Symbolic Bounded Synthesis

Synthesis of finite state systems from full linear time temporal logic (LTL) specifications is gaining more and more attention as several achievements in the last years have significantly improved its practical applicability. Recent works in this area are based on the Safraless synthesis approach and either perform the computation in an explicit way or use symbolic data structures other than binary decision diagrams (BDDs). In this paper, we close this gap and consider Safraless synthesis using BDDs as state space representation. The key to this combination is the application of novel optimisation techniques, which decreases the number of state bits in such a representation significantly. We evaluate our approach on several practical benchmarks, including a new load balancing case study. Our experiments show an improvement of several orders of magnitude over previous approaches.

10:55 Krishnendu Chatterjee, Thomas Henzinger, Barbara Jobstmann and Rohit Singh
Measuring and Synthesizing Systems in Probabilistic Environments

Often one has a preference order among the different systems that satisfy a given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal-synthesis problem: given an omega-regular specification, a Markov chain that describes the distribution of inputs, and a weighted automaton that measures how well a system satisfies the given specification under the given input assumption, synthesize a system that optimizes the measured value.

For safety specifications and measures that are defined by mean-payoff automata, the optimal-synthesis problem amounts to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be done in polynomial time. For general omega-regular specifications, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives. We also present some experimental results showing optimal systems that were automatically generated in this way.

11:20 Susanne Graf, Doron Peled and Sophie Quinton
Achieving Distributed Control Through Model Checking

We apply model checking of knowledge properties to the design of distributed controllers that enforce global constraints on concurrent systems. The problem of synthesizing a distributed controller is, in general, undecidable, and the local knowledge of the processes may not directly suffice to control them to achieve the global constraint. We calculate when processes can decide, autonomously, to take or block an action so that the global constraint will not be violated. When the separate processes cannot make this decision alone, it may be possible to coordinate several processes in order to achieve more knowledge together and make combined decisions. A fixed coordination will severely degrade the concurrency. Thus, the coordinations we suggest to impose are temporary. Since the overhead for such coordinations is expensive, we strive to minimize their number, again using model checking. We show how this framework is applied to the design of controllers that guarantee a priority policy among transitions.

11:45 Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas Henzinger and Barbara Jobstmann
Robustness in the Presence of Liveness

Systems ought to behave reasonably even in circumstances that are not anticipated in their specifications. We propose a definition of robustness for liveness specifications which prescribes, for any num- ber of environment assumptions that is violated, a minimal number of system guarantees that must still be fulfilled. This notion of robustness can be formulated and realized using a Generalized Reactivity formula We present an algorithm for synthesizing robust systems from such for- mulas. For the important special case of Generalized Reactivity formulas of rank 1, our algorithm improves the complexity for large specifications with a small number of assumptions and guarantees.

12:10 Roderick Bloem, Alessandro Cimatti, Karin Greimel, Georg Hofferek, Robert Koenighofer, Marco Roveri, Viktor Schuppan and Richard Seeber
RATSY - A new Requirements Analysis Tool with Synthesis

Formal specifications play an increasingly important role in system design-flows. Yet, they are not always easy to deal with. In this paper we present RATSY, a successor of the Requirements Analysis Tool RAT. RATSY extends RAT in several ways. First, it includes a new graphical user interface to specify system properties as simple Buechi word automata. Second, it can help debug incorrect specifications by means of a game-based approach. Third, it allows correct-by-construction synthesis of systems from their temporal properties. These new features and their seamless integration assist in property-based design processes.

12:25 Viktor Kuncak, Mikael Mayer, Ruzica Piskac and Philippe Suter
Comfusy: A Tool for Complete Functional Synthesis

Synthesis of program fragments from specications can make programs easier to write and easier to reason about. We present Comfusy, a tool that extends the compiler for the general-purpose programming language Scala with (non-reactive) functional synthesis over unbounded domains. Comfusy accepts expressions with input and output variables specifying relations on integers and sets. Comfusy computes the weakest precondition for the given relation and generates the function from inputs to outputs that satisfy the relation whenever the precondition holds. The core of our synthesis algorithm is an extension of quantifier elimination that generates programs to compute witnesses for eliminated variables. We present examples that demonstrate software synthesis using Comfusy and illustrate how synthesis simplifies software development.

14:00‑15:00 FLoC Keynote Talk: Deepak Kapur
Location: George Square Lecture Theatre
14:00 Deepak Kapur (University of New Mexico)
Induction, Invariants, and Abstraction

Invariants play a key role in verifying properties of imperative programs. Inductive reasoning is essential to verifying properties of recursive programs. Relationship between derivation of loop invariants and speculation of lemmas in inductive reasoning is explored. Abstraction is an effective heuristic for approximating program behavior in order to derive invariants. Interaction among developing abstractions, inductive reasoning, and generating invariants is investigated.

15:30‑17:35 Concurrent Program Verification I
Chair: Azadeh Farzan
Location: AT LT4
15:30 Vineet Kahlon and Chao Wang
Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs

Triggering errors in concurrent programs is a notoriously difficult task. A key reason for this is the behavioral complexity resulting from the large number of interleavings of operations of different threads. Efficient static techniques, therefore, play a critical role in restricting the set of interleavings that need be explored in depth. The goal here is to exploit scheduling constraints imposed by synchronization primitives to determine whether the property at hand can be violated and propose schedules that may lead to such a violation. Towards that end, we propose the new notion of a Universal Causality Graph (UCG) that given a correctness property P, encodes the set of all (statically) feasible interleavings that may violate P. UCGs provide a unified happens-before model by reducing causality constraints imposed by the property at hand as well as scheduling constraints imposed by synchronization primitives to causality constraints. Embedding all these constraints into one common framework allows us to exploit the synergy between constraints imposed by different synchronization primitives, as well as between constraints imposed by the property and the primitives. This enables us to filter out more redundant interleavings than would otherwise be possible. Importantly, it also guarantees both soundness and completeness of our technique. Unlike the existing state-of-the-art, our new technique has all of the following desirable features: (i) works for all the standard synchronization primitives, (ii) is exact, (iii) exploits causality constraints induced by the primitives as well as the property, and (iv) is scalable for predictive analysis. As application, we demonstrate the use of UCGs in enhancing the precision and scalability of predictive analysis in the context of runtime verification of concurrent programs.

15:55 Viktor Vafeiadis
Automatically proving linearizability

We present a practical, automatic verification procedure for proving linearizability (i.e. functional correctness) of concurrent data structure implementations, and evaluate it on a number of concurrent stack, queue and set algorithms from the literature.

16:20 Pavol Cerny, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri and Rajeev Alur
Model Checking of Linearizability of Concurrent List Implementations
16:45 Ernie Cohen, Michał Moskal, Stephan Tobies and Wolfram Schulte
Local Verification of Global Invariants in Concurrent Programs

We describe a practical method for reasoning about realistic concurrent programs. Our method allows global two-state invariants that restrict update of shared state. We provide simple, sufficient conditions for checking those global invariants modularly. The method has been implemented in VCC, an automatic, sound, modular verifier for concurrent C programs. VCC has been used to verify tens of thousands of lines of Microsoft's Hyper-V virtualization platform and of SYSGO's embedded real-time operating system PikeOS.

17:10 Aws Albarghouthi, Arie Gurfinkel, Ou Wei and Marsha Chechik
Abstract Analysis of Symbolic Executions

Multicore technology has moved concurrent programming to the forefront of computer science. In this paper, we look at the problem of reasoning about concurrent systems with infinite data domains and non-deterministic input, and develop a method for verification and falsification of safety properties of such systems. Novel characteristics of this method are (a) constructing under-approximating models via symbolic execution with abstract matching and (b) proving safety using under-approximating models.

17:35‑17:50 Competition Results
Location: AT LT4
17:35 Clark Barrett, Morgan Deters, Albert Oliveras and Aaron Stump
Report on SMT-COMP 2010