CAV on Friday, July 16th

09:00‑10:00 FLoC Plenary Talk: David Basin
Location: George Square Lecture Theatre
09:00 David Basin (ETH Zurich)
Policy Monitoring in First-order Temporal Logic

In security and compliance, it is often necessary to ensure that agents and systems comply to complex policies. An example from financial reporting is the requirement that every transaction t of a customer c, who has within the last 30 days been involved in a suspicious transaction t', must be reported as suspicious within 2 days. We present an approach to monitoring such policies formulated in an expressive fragment of metric first-order temporal logic. We also report on case studies in security and compliance monitoring and use these to evaluate both the suitability of this fragment for expressing complex, realistic policies and the efficiency of our monitoring algorithm.

(Joint work with Felix Klaedtke and Samuel Mueller)

10:30‑12:30 Software Model Checking
Chair: Orna Grumberg
Location: AT LT4
10:30 Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Ahmed Rezine and Mihaela Sighireanu
Invariant Synthesis for Programs Manipulating Lists with Unbounded Data

We address the issue of automatic program invariant synthesis. We propose a method based on abstract reachability analysis for programs manipulating dynamic singly-linked lists with data over infinite domains such as integers. The specifications of programs with dynamic heaps naturally constrain various aspects such as the sizes of list segments in the heap structure, the sets (or multisets) of elements in these segments, or the sequences of values attached to these segments. In some cases, complex relations between the sizes and the values in the structures (or even some combinations of these values such as their sum) are needed. Our framework allows to define abstract domains which capture these various aspects. The abstract domains we consider are defined in a parametric way, and combine an abstraction of the heap graph with an abstraction of the data sequences attached to the segments of this graph. As an instance of this generic definition, we introduce a new abstract domain for reasoning about vectors of data sequences over an infinite alphabet (e.g., integers) where objects are universally quantified first-order formulas. Moreover, we define sound abstract transformers for the statements in the class of programs we consider, and propose sufficient conditions under which they are best transformers. Our techniques are able to synthesize automatically complex invariants for a wide class of programs. We provide experimental results showing the efficiency of our approach.

10:55 Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich and Christoph M.Wintersteiger
Termination Analysis with Compositional Transition Invariants
11:20 Kenneth McMillan
Lazy Annotation for Program Testing and Verification

We describe an interpolant-based approach to test generation and model checking for sequential programs. The method generates Floyd/Hoare style annotations of the program on demand, as a result of failure to achieve goals, in a manner analogous to conflict clause learning in a DPLL style SAT solver. Relative to earlier interpolant-based approaches, this method has the advantage that it can generate procedure summaries and handle recursive functions. Moreover, because it explores only feasible paths, it is easily adaptable to test generation, and handles fixed-bounded loops efficiently. Compared to partition refinement methods, the method is fully symbolic, and less prone to divergence for unbounded loops. We demonstrate the approach on the problem of generating tests with complete basic block coverage for device driver examples.

11:45 Thomas Ball, Ella Bounimova, Vladimir Levin, Rahul Kumar and Jakob Lichtenberg
The Static Driver Verifier Research Platform
12:00 Ming Kawaguchi, Patrick M. Rondon and Ranjit Jhala
Dsolve: Verification Via Liquid Type Inference

We present Dsolve, a software verification tool for OCaml based on refinement type inference. Traditionally, verification with refinement types has been impractical due to the heavy burden of manually annotating a program with refined types. Using Liquid Types, Dsolve significantly eases this burden by inferring refinement types expressive enough to verify a variety of complex program safety properties.

12:15 Sudipta Kundu, Malay Ganai and Chao Wang
CONTESSA: Concurrency Testing Augmented with Symbolic Analysis

Testing of multi-threaded programs poses enormous challenges. For most programs, there are numerous thread interleaving, and testing the program's behavior for each interleaving is infeasible. To improve the coverage of testing, and to strike a balance between efficiency and scalability, we present a framework named "CONTESSA" that augments testing (concrete execution) with symbolic analysis to explore both thread interleaving and input data space. It is built on several innovative techniques---such as token-based modeling and partial-order reduction techniques---to generate verification conditions (SMT formulas) that can be solved by the current SMT solvers with relative ease. It also provides a visual support for debugging the witness traces. We illustrate the significance of such a framework in testbeds.

14:00‑14:50 Model Checking and Automata
Chair: Roderick Bloem
Location: AT LT4
14:00 Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukas Holik, Chih-Duo Hong, Richard Mayr and Tomas Vojnar
Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing

There are two main classes of methods for checking universality and language inclusion of Büchi-automata: Rank-based methods and Ramsey-based methods. While rank-based methods have a better worst-case complexity, Ramsey-based methods have been shown to be quite competitive in practice [1,2]. It was shown in [1] (for universality checking) that a simple subsumption technique, which avoids exploring certain cases, greatly improves the performance of the Ramsey-based method. Here, we present a much more general subsumption technique for the Ramsey-based method, which is based on using simulation preorder on the states of the Büchi-automata. This technique applies to both universality and inclusion checking, yielding a substantial performance gain over the previous simple subsumption approach of [1].

1. S. Fogarty and M. Y. Vardi. Efficient Büchi Universality Checking. To appear in Proc. of TACAS'10. 2. S. Fogarty and M. Y. Vardi. Büchi Complementation and Size-Change Termination. In Proc. of TACAS'09, LNCS 5505, 2009.

14:25 Frédéric Herbreteau, B Srivathsan and Igor Walukiewicz
Efficient Emptiness Check for Timed Büchi Automata

The Büchi non-emptiness problem for timed automata concerns deciding if a given automaton has an infinite non-Zeno run satisfying the Büchi accepting condition. The standard solution to this problem involves adding an auxiliary clock to take care of the non-Zenoness. In this paper, we show that this simple transformation may sometimes result in an exponential blowup. We propose a method avoiding this blowup.

15:30‑16:30 Tools
Chair: David Monniaux
Location: AT LT4
15:30 Nicolas Caniart
Merit: an Interpolating Model-Checker

We present the tool Merit, a Cegar model-checker for safety properties of counter-systems, which sits in the Lazy Abstraction with Interpolants (Lawi) framework. Lawi is parametric with respect to the interpolation technique and so is Merit. Thanks to its open architecture, Merit makes it possible to experiment new refinement techniques without having to re-implement the generic, technical part of the framework. In this paper, we first recall the basics of the Lawi algorithm. We then explain two heuristics in order to help termination of the Cegar loop: the first one presents different approaches to symbolically compute interpolants. The second one focuses on how to improve the unwinding strategy. We finally report our experimental results on a large amount of classical models.

15:45 Alexandre Donzé
Breach, A Simulation-based Toolbox for the Verification and Parameter Synthesis of Hybrid Systems

We describe \Breach, a Matlab toolbox which intends to provide a coherent set of techniques for the analysis of deterministic models of hybrid dynamical systems. These techniques are simulation-based, meaning that the primary feature of \Breach is to greatly facilitate the computation, manipulation and investigation of possibly large sets of trajectories. It relies on a robust and efficient numerical solver of ordinary differential equations that can also provide information about sensitivity with respect to parameters uncertainty. This is used at a higher level to perform approximate reachability analysis and parameter synthesis, i.e., to generate subsets of parameters for which the system satisfies a desired safety property. This version introduces two major novel features: a rich graphical user interface, and the robust monitoring of metric interval temporal logic (MITL) formulas. The application domain of \Breach is wide, ranging from embedded system design using Simulink, to the analysis of complex nonlinear models issued from systems biology.

16:00 Amir Pnueli, Yaniv Sa'ar and Lenore D. Zuck
JTLV : A Framework for Developing Verification Algorithms

Most existing verification tools are designed to serve as verifiers where, to implement all but the simplest verification algorithm, a developer of the algorithm is assumed to be intimately familiar with the internal structure and implementation details of the underlying verification system. For reasons of efficiency, verification systems are commonly implemented in a low-level C code.

We present JTLV. JTLV provides an abstract framework for developing verification applications in a high-level programming environment. JTLV allows the developer of the verification algorithm to focus his goals at hand without sacrificing performance or dealing with low-level details.

16:15 Roland Meyer and Tim Strazny
Petruchio: From Dynamic Networks to Nets

We introduce Petruchio, a tool for computing Petri net translations of dynamic networks. To cater for unbounded architectures beyond the capabilities of existing implementations, the principle fixed-point engine runs interleaved with coverability queries. We discuss algorithmic enhancements and provide experimental evidence that Petruchio copes with models of reasonable size.

16:30‑18:00 In Memory of Amir Pnueli
Chair: Doron Peled
Location: AT LT4
16:30 Moshe Vardi
Amir Pnueli: Ahead of His Time
17:30 Doron Peled, Zohar Manna and others
Reminiscences on Amir Pnueli (TBC)