CAV on Sunday, August 20th

Invited Talk (09:00‑10:00)
Chair: Robert Jones

09:00‑10:00

Joe Stoy (Bluespec) Verification? Getting it Right the First Time [ppt] ...

Break (10:00‑10:30)

Session 15: Abstract Interpretation (10:30‑12:00)
Chair: Robert Jones

10:30‑11:00	Shuvendu Lahiri (Microsoft) Robert Nieuwenhuis (Tech. University Catalonia) Albert Oliveras (Tech. Univ. Catalonia, Barcelona) SMT Techniques for Predicate Abstraction Predicate abstraction is a technique for automatically extracting finite-state abstractions for systems with potentially infinite state space. The fundamental operation in predicate abstraction is to compute the best approximation of a Boolean formula F over a set of predicates P. In this work, we demonstrate the use for this operation of a decision procedure based on the DPLL(T) framework for SAT Modulo Theories (SMT). The new algorithm is based on a careful generation of the set of all satisfying assignments over a set of predicates. It consistently outperforms previous methods by a factor of at least 20, on a diverse set of hardware and software verification benchmarks. We also report detailed analysis of the results and the impact of a number of variations of the techniques.
11:00‑11:30	Bernard Boigelot (Université de Liège) Frédéric Herbreteau (LaBRI) The Power of Hybrid Acceleration This paper addresses the problem of computing symbolically the set of reachable configurations of a linear hybrid automaton. A solution proposed in earlier work consists in exploring the reachable configurations using an acceleration operator for computing the iterated effect of selected control cycles. Unfortunately, this method imposes a periodicity requirement on the data transformations labeling these cycles, that is not always satisfied in practice. This happens in particular with the important subclass of timed automata, even though it is known that the paths of such automata have a periodic behavior. The goal of this paper is to broaden substantially the applicability of hybrid acceleration. This is done by introducing powerful reduction rules, aimed at translating hybrid data transformations into equivalent ones that satisfy the periodicity criterion. In particular, we show that these rules always succeed in the case of timed automata. This makes it possible to compute an exact symbolic representation of the set of reachable configurations of a linear hybrid automaton, with a guarantee of termination over the subclass of timed automata. Compared to other known solutions to this problem, our method is simpler, and applicable to a much larger class of systems. As a secondary contribution, we also provide a simpler, as well as constructive, proof of an acceleration result due to Comon and Jurski.
11:30‑12:00	Denis Gopan (University of Wisconsin) Thomas Reps (University of Wisconsin; GrammaTech, Inc.) Lookahead Widening We present lookahead widening, a novel technique for using existing widening and narrowing operators to improve the precision of static analysis. This technique is both self-contained and fully-automatic in the sense that it does not rely on separate analyzes or human involvement. We show how to integrate lookahead widening into existing analyzers with minimal effort. Experimental results indicate that the technique is able to achieve sizable precision improvements at reasonable costs.

Session 16: Tools Papers (12:00‑12:30)
Chair: Robert Jones

12:00‑12:15

Kenneth Roe (To be announced) The Heuristic Theorem Prover: Yet another SMT Modulo Theorem Prover In recent years, there has been considerable interest in developing theorem provers that integrate SAT solving algorithms with decision procedures for domain theories such as linear arithmetic, arrays, equality of uninterpreted function symbols and bit vector arithmetic. The main contribution of HTP is the introduction of a preprocessor that includes algorithms for detecting unate predicates, eliminating variables and doing symmetry analysis. The other algorithms of HTP are similar to many other systems. HTP implements a DPLL(T) with exhaustive theory propagation similar to BarcelogicTools. There are domain theories for equality of uninterpreted function symbols, and real difference logic. HTP has an incomplete implementation of linear inequality and array decision procedures. As input, HTP accepts problems using the SMT-LIB format. As output, HTP will answer either SAT, UNSAT or UNKNOWN. An evidence file showing the derivation in a human readable form can be produced. There is a Treeview application which shows this derivation in a tree widget making it convenient to navigate a complex proof.

12:15‑12:30

Abhay Vardhan (Google, Inc.) Mahesh Viswanathan (University of Illinois, Urbana-Champaign) LEVER: A tool for Learning Based Verification We present a tool called LEVER which implements a new method for verification of infinite state systems using techniques from computational learning theory. LEVER can analyze safety properties as well as liveness properties using either Computational Tree Logic with fairness constraints or omega-regular languages. We give some details about the tool and discuss results of running LEVER on some interesting examples. We also compare LEVER with some other tools that are available for verification of infinite state systems.

Lunch break (12:30‑14:00)

Session 17: Memory Consistency (14:00‑15:30)
Chair: Ganesh Gopalakrishnan

14:00‑14:30	Robert Colvin (University of Queensland) Lindsay Groves (Victoria University of Wellington) Victor Luchangco (Sun Microsystems) Mark Moir (Sun Microsystems) Formal Verification of a Lazy Concurrent List-Based Set We describe a formal verification of a recent concurrent list-based set algorithm due to Heller et al. The algorithm is optimistic: the add and remove operations traverse the list without locking, and lock only the nodes affected by the operation; the contains operation uses no locks and is wait-free. These properties make the algorithm challenging to prove correct, much more so than simple coarse-grained locking algorithms. We have proved that the algorithm is linearisable, using simulations between input/output automata modelling the behaviour of an abstract set and the implementation. The automata and simulation proof obligations are specified and verified using PVS.
14:30‑15:00	Sebastian Burckhardt (University of Pennsylvania) Rajeev Alur (University of Pennsylvania) Milo M.K. Martin (University of Pennsylvania) Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study Concurrent data type implementations are commonly used by programs written for shared-memory multiprocessors. Their verification poses additional challenges compared to mainstream multi-threaded software: (1) the correctness condition, sequential consistency, is not a regular property; and (2) on relaxed memory models, multiprocessor executions exhibit a high degree of concurrency at the instruction level. In this case study, we investigate how to apply SAT-based model checking to this problem. First, we choose a representative implementation, the two-lock concurrent queue by Michael and Scott. Next, we define a relaxed memory model that is a conservative approximation of several models used by common server architectures. Using commit point specifications, a suite of finite symbolic client programs, a prototype encoder, and a standard SAT solver, we successfully identify two failures of a naive implementation that can be observed only under relaxed memory models. We fix these failures by inserting appropriate memory ordering barriers into the code. The results are overall encouraging: they confirm the practical value and adequate scalability of our approach.
15:00‑15:30	Amitabha Roy (Intel Corporation) Chuck Fleckenstein (Intel Corporation) Stephan Zeisset (Intel Corporation) John Huang (University of Michigan) Fast and Generalized Polynomial Time Memory Consistency Verification The problem of verifying multi-threaded execution against the memory consistency model of a processor is known to be an NP hard problem. However polynomial time algorithms exist that detect almost all failures in such execution. These are often used in practice for microprocessor verification. We present a low complexity and fully parallelized algorithm to check program execution against the processor consistency model. In addition our algorithm is general enough to support a number of consistency models without any degradation in performance. This implementation of this algorithm is currently used in practice to verify processors in the post silicon stage for multiple architectures.

Break (15:30‑16:00)

Session 18: Shape Analysis (16:00‑17:30)
Chair: Thomas Ball

16:00‑16:30	Radu Iosif (Verimag) Marius Bozga (Verimag) Ahmed Bouajjani (Liafa) Peter Habermehl (Liafa) Pierre Moro (Liafa) Tomas Vojnar (Brno University of Technology) Programs with Lists are Counter Automata We address the verification problem of programs manipulating one-selector linked data structures. We propose a new automated approach for checking safety and termination for these programs. Our approach is based on using counter automata as accurate abstract models: control states correspond to abstract heap graphs where list segments without sharing are collapsed, and counters are used to keep track of the number of elements in these segments. This allows to apply automatic analysis techniques and tools for counter automata in order to verify list programs. We show the effectiveness of our approach, in particular by verifying automatically termination of some sorting programs.
16:30‑17:00	Dirk Beyer (EPFL) Tom Henzinger (EPFL) Grégory Théoduloz (EPFL) Lazy Shape Analysis Many software model checkers are based on predicate abstraction. Values of variables in branching conditions are represented abstractly using predicates. The strength of this approach is its path-sensitive nature. However, if the control flow depends heavily on the values of memory cells on the heap, the approach does not work well, because it is difficult to find `good' predicate abstractions to represent the heap. In contrast, shape analysis can lead to a very compact representation of data structures stored on the heap. In this paper, we combine shape analysis with predicate abstraction, and integrate it into the software model checker BLAST. Because shape analysis is expensive, we do not apply it globally. Instead, we ensure that shapes are computed and stored locally, only where necessary for proving the verification goal. To achieve this, we extend lazy abstraction refinement, which so far has been used only for predicate abstractions, to shapes. This approach does not only increase the precision of model checking and shape analysis taken individually, but also increases the efficiency of shape analysis (we do not compute shapes where not necessary). We implemented the technique by extending BLAST with calls to TVLA, and evaluated it on several C programs manipulating data structures, with the result that the combined tool can now automatically verify programs that are not verifiable using either shape analysis or predicate abstraction on its own.
17:00‑17:30	Tal Lev-Ami (Tel-Aviv University, Israel) Neil Immerman (UMass, Amherst) Mooly Sagiv (Tel Aviv University) Abstraction for Shape Analysis with Fast and Precise Transformers This paper addresses the problem of proving safety properties of imperative programs manipulating dynamically allocated data structures using destructive pointer updates. We present a new abstraction for linked data structures whose underlying graphs do not contain cycles. The abstraction is simple and allows us to decide reachability between dynamically allocated heap cells. We present an efficient algorithm that computes the effect of low level heap mutations in the most precise way. The algorithm does not rely on the usage of a theorem prover. In particular, the worst case complexity of computing a single successor abstract state is O(V *log V) where V is the number of program variables. The overall number of successor abstract states can be exponential in V. A prototype of the algorithm was implemented and is shown to be fast. Our method also handles programs with "simple cycles" such as cyclic singly-linked lists, (cyclic) doubly-linked lists, and trees with parent pointers. Moreover, we allow programs which temporarily violate these restrictions as long as they are restored in loop boundaries.

SMT-COMP report (17:30‑17:45)
Chair: Clark Barrett, Aaron Stump, Leonardo de Moura