CAV on Saturday, August 19th

Session 11: Concurrency (09:00‑10:30)
Chair: Ahmed Bouajjani

09:00‑09:30	Vineet Kahlon (NEC Laboratories, Princeton) Aarti Gupta (NEC Laboratories USA) Nishant Sinha (Carnegie Mellon University) Symbolic Model Checking of Concurrent Programs using Partial Orders and On-the-fly Transactions The state explosion problem is one of the core bottlenecks in the model checking of concurrent software. We show how to ameliorate the problem by combining the ability of partial order techniques to reduce the state space of the concurrent program with the power of symbolic model checking to explore large state spaces. Our new verification methodology involves translating the given concurrent program into a circuit-based model which gives us the flexibility to then employ any model checking technique of choice -- either SAT or BDD-based -- for verifying a broad range of linear time properties, not just safety. The reduction in the explored state-space is obtained by statically augmenting the symbolic encoding of the program by additional constraints. These constraints restrict the scheduler to choose from a minimal conditional stubborn set of transitions at each state. Another key contribution of the paper, is a new method for detecting transactions on-the-fly which takes into account patterns of lock acquisition and yields better reductions than existing methods which rely on a lockset based analysis. Moreover unlike existing techniques, identifying on-the-fly transactions does not require the program to follow a lock discipline in accessing shared variables. We have applied our techniques to the Daisy test bench and shown the existence of several bugs.
09:30‑10:00	Koushik Sen (University of Illinois at Urbana Champaign) Mahesh Viswanathan (University of Illinois, Urbana-Champaign) Model Checking Multithreaded Programs with Asynchronous Atomic Methods In order to make multithreaded programming manageable, programmers often follow a design principle where they break the problem into tasks which are then solved asynchronously and concurrently on different threads. This paper investigates the problem of model checking programs that follow this idiom. We present a programming language SPL that encapsulates this design pattern. SPL extends simplified form of sequential Java to which we add the capability of making asynchronous method invocations in addition to the standard synchronous method calls and the ability to execute asynchronous methods in threads atomically and concurrently. Our main result shows that the control state reachability problem for finite SPL programs is decidable. Therefore, such multithreaded programs can be model checked using the counter-example guided abstraction-refinement framework.
10:00‑10:30	Azadeh Farzan (University of Illinois at Urbana-Champaign) P. Madhusudan (University of Illinois at Urbana-Champaign) Causal Atomicity Atomicity is an important generic specification that many correct concurrent programs adhere to. Intuitively, atomicity of a program block assures the programmer can pretend that the block occurs sequentially in any execution. Our main contribution is a notion of atomicity based on causality. We model the control flow of a program with threads using a Petri net that naturally captures the independence of threads, the interactions between them, and the abstraction of data. The partially ordered executions of the Petri net are then endowed with a causality relation between events; we exploit this to define our notion of causal atomicity. We show that causal atomicity is a robust notion that many programs follow, and show how we can effectively check causal atomicity using Petri net tools based on unfoldings, which exploit the concurrency in the net to yield automatic partial-order reduction in the state-space.

Break (10:30‑11:00)

Session 12: Trees, Pushdown Systems and Boolean Programs (11:00‑12:30)
Chair: Ranjit Jhala

11:00‑11:30	Rajeev Alur (University of Pennsylvania) Swarat Chaudhuri (University of Pennsylvania) P. Madhusudan (University of Illinois at Urbana-Champaign) Languages of Nested Trees We study languages of nested trees — structures obtained by augmenting trees with sets of nested jump-edges. These graphs can naturally model branching behaviors of pushdown programs, so that the problem of branching-time software model checking may be phrased as a membership question for such languages. We define finite-state automata accepting such languages — these automata can pass states along jump-edges as well as tree edges. We find that the model-checking problem for these automata on pushdown systems is EXPTIME-complete, and that their alternating versions are expressively equivalent to NT-mu, a recently proposed temporal logic for nested trees that can express a variety of branching-time, ``context-free'' requirements. We also show that monadic second order logic (MSO) cannot exploit the structure: MSO on nested trees is too strong in the sense that it has an undecidable model checking problem, and seems too weak to capture NT-mu.
11:30‑12:00	Akash Lal (University of Wisconsin) Thomas Reps (University of Wisconsin; GrammaTech, Inc.) Improving Pushdown System Model Checking In this paper, we reduce pushdown system (PDS) model checking to a graph-theoretic problem, and apply a fast graph algorithm to improve the running time for model checking. Several other PDS questions and techniques can be carried out in the new setting, including witness tracing and incremental analysis, each of which benefits from the fast graph-based algorithm.
12:00‑12:30	Andreas Griesmayer (TU Graz / Institute for Software Technology) Roderick Bloem (TU Graz / Institute for Software Technology) Byron Cook (Microsoft Research) Repair of Boolean Programs with an Application to C We show how to find and fix faults in Boolean programs by extending the program to a game. In the game, the protagonist can select alternative behavior for an incorrect statement. If the protagonist can do so successfully using a memoryless strategy that does not depend on the stack contents, we have found a correction for the Boolean program. We present a symbolic algorithm that localizes possibly faulty statements and provides corrections. If the Boolean program is an abstraction of a C program, the repair for the Boolean program suggests a repair for the original C program. This yields a heuristic approach to repairing C programs. We have applied this idea to Boolean programs that are produced as abstractions by SLAM and have thus successfully patched several faulty Windows device drivers written in C.

Lunch (in hotel) (12:30‑14:00)
Location: Grand Ballroom D

Session 13: Termination (14:00‑15:30)
Chair: Thomas Ball

14:00‑14:30	Mark Braverman (University of Toronto) Termination of Integer Linear Programs We show that termination of a simple class of linear loops over the integers is decidable. Namely we show that termination of deterministic linear loops is decidable over the integers in the homogeneous case, and over the rationals in the general case. This is done by analyzing the powers of a matrix symbolically using its eigenvalues. Our results generalize the work of Tiwari [Tiw04], where similar results were derived for termination over the reals. We also gain some insights into termination of non-homogeneous integer programs, that are very common in practice.
14:30‑15:00	Josh Berdine (Microsoft Research, Cambridge) Byron Cook (Microsoft Research) Dino Distefano (Queen Mary, University of London) Peter O'Hearn (Queen Mary, University of London) Automatic termination proofs for programs with shape-shifting heaps We describe a new program termination analysis designed to handle imperative programs whose termination depends on the mutation of the program's heap. We first describe how an abstract interpretation can be used to construct a finite number of relations which, if each is well-founded, implies termination. We then give an abstract interpretation based on separation logic formulae which tracks the depths of pieces of heaps. Finally, we combine these two techniques to produce an automatic termination prover. We show that the analysis is able to prove the termination of loops extracted from Windows device drivers that could not be proved terminating before by other means; we also discuss a previously unknown bug found with the analysis.
15:00‑15:30	Panagiotis Manolios (Georgia Tech) Daron Vroon (Georgia Institute of Technology, College of Computing) Termination Analysis with Calling Context Graphs We introduce calling context graphs and various static and theorem proving based analyses that together provide a powerful method for proving termination of programs written in feature-rich, first order, functional programming languages. In contrast to previous work, our method is highly automated and handles any source of looping behavior in such languages, including recursive definitions, mutual recursion, the use of recursive data structures, etc. We have implemented our method for the ACL2 programming language and evaluated the result using the ACL2 regression suite, which consists of numerous libraries with a total of over 10,000 function definitions. Our method was able to automatically detect termination of over 98% of these functions.

Session 14: Tools Papers (15:30‑16:00)
Chair: Thomas Ball

15:30‑15:45

Byron Cook (Microsoft Research) Andreas Podelski (MPI) Andrey Rybalchenko (Max-Planck Institut für Informatik) Terminator: Beyond Safety Previous symbolic software model checkers (i.e., program analysis tools based on predicate abstraction, pushdown model checking and iterative counterexample-guided abstraction refinement, etc.) are restricted to safety properties. TERMINATOR is the first software model checker for termination. It is now being used to prove that device driver dispatch routines always return to their caller (or return counterexamples if they don't).

15:45‑16:00

Koushik Sen (University of Illinois at Urbana Champaign) Gul Agha (University of Illinois at Urbana Champign) CUTE and jCUTE : Concolic Unit Testing and Explicit Path Model-Checking Tools CUTE, a Concolic Unit Testing Engine for C and Java, is a tool to systematically and automatically test sequential C programs (including pointers) and concurrent Java programs. CUTE combines concrete and symbolic execution in a way that avoids redundant test cases as well as false warnings. The tool also introduces a race-flipping technique to efficiently test and model check concurrent programs with data inputs.

Break (16:00‑16:30)

Keynote Session (16:30‑17:30)
Chair: Wolfram Schulte, Moshe Vardi
Location: Grand Ballroom B/C

16:30‑17:30

David Harel (Weizmann Institute) Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs [ppt] We concentrate on executing scenario-based, inter-object programs. The basic play-out method for live sequence charts (LSCs), which we proposed several years ago and implemented in the Play-Engine tool, deals with the nondeterminism inherent in such programming like racing conditions. It thus cannot correct unsuccessful choices it makes. The talk discusses three more recent and more sophisticated ways to run LSCs, and by extension to execute scenario-based models and programs in general. Interestingly, and somewhat unusually, these three methods use, respectively, ideas from three quite separate fields of computer science: verification (model-checking), artificial intelligence (planning algorithms) and programming methods (Aspect-oriented programming).

CAV Business Meeting (18:00‑19:00)