CAV on Monday, July 19th

09:00‑10:00 Invited Talk
Chair: Markus Mueller-Olm
Location: AT LT4
09:00 Maged Michael
Memory Management in Concurrent Algorithms
10:30‑12:00 Compositional Reasoning
Chair: Natasha Sharygina
Location: AT LT4
10:30 Yu-Fang Chen, Edmund Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay and Bow-Yaw Wang
Automated Assume-Guarantee Reasoning through Implicit Learning

We propose a purely implicit solution to the contextual assumption generation problem in assume-guarantee reasoning. Instead of improving the explicit $L^*$ algorithm, the Boolean functions implicitly representing contextual assumptions are computed in our algorithm. We report parametrized test cases where our solution outperforms the monolithic interpolation-based Model Checking algorithm.

10:55 Rishabh Singh, Dimitra Giannakopoulou and Corina Pasareanu
Learning Component Interfaces with May and Must Abstractions

Component interfaces are the essence of modular program analysis. In this work, a component interface documents correct sequences of invocations to the component's public methods. We present a novel and fully automated framework that automatically and efficiently extracts finite interfaces that are safe, permissive, and minimal, from potentially infinite software components. Our proposed framework uses the L* automata-learning algorithm to directly learn finite interfaces for an infinite-state component. It is based on the observation that an interface permissive with respect to the component's must abstraction and safe with respect to its may abstraction provides a precise characterization of the legal invocations to the methods of the concrete component. The abstractions are refined automatically from counterexamples obtained during reachability checks performed by our framework. The use of must abstractions enables us to avoid an exponentially expensive determinization step that is required when working with may abstractions only, and the use of L* guarantees minimality of the generated interface. We have implemented the algorithm in the predicate-abstraction-based model checker ARMC, and report on its application to a number of case studies including several Java2SDK and J2SEE library classes. We also report on the successful application of our algorithm for generating interfaces for NASA flight-software components.

11:20 Ariel Cohen, Kedar Namjoshi and Yaniv Sa'ar
A Dash of Fairness for Compositional Reasoning

Proofs of progress properties often require fairness assumptions. Incorporating global fairness assumptions in compositional methods is a challenge given the local flavor of such reasoning. We present a fully automated local reasoning algorithm which handles fairness assumptions. Since local reasoning is incomplete, the algorithm includes a refinement step which strengthens local proofs by adding auxiliary variables. Experiments show that verification with the local algorithm is often significantly faster than with standard model checking.

11:45 Ariel Cohen, Kedar Namjoshi and Yaniv Sa'ar
SPLIT: A Compositional LTL Verifier

This paper describes SPLIT, a compositional LTL verifier for shared-variable, multi-threaded programs. SPLIT implements the techniques of \cite{namjoshi-07a,cohen-namjoshi07,cohen-namjoshi08,cohen-saar-namjoshi10} for verifying safety and general LTL properties. The foundation is a computation of compact local invariants, one for each process, that are used for constructing a proof for the property. If the invariants are too weak, an automatic refinement gradually exposes more local information, until the property can be proved or a valid counter example is formed.

12:00‑12:30 Tool Session
Chair: Holger Hermanns
Location: AT LT4
12:00 Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri and Ralf Wimmer
A Model Checker for AADL

We present a graphical toolset for verifying AADL models, which are gaining widespread acceptance in aerospace, automobile and avionics industry for modelling safety-critical systems comprehensively by capturing functional, probabilistic and hybrid aspects coherently. The analyses are implemented on top of mature model checking tools and range from requirements validation to functional verification, safety assessment via automatic derivation of FMEA tables and dynamic fault trees, performability evaluation, diagnosis and diagnosability. It is currently being applied to several case studies by a major industrial developer of aerospace systems.

12:15 Manuel Mazo Jr., Anna Davitian and Paulo Tabuada
PESSOA: A tool for embedded controller synthesis.

In this paper we present Pessoa, a tool for the synthesis of correct-by-design embedded control software. Pessoa relies on recent results on approximate abstractions of control systems to reduce the synthesis of control software to the synthesis of reactive controllers for finite-state models. We describe the capabilities of Pessoa and illustrate them through an example.

14:00‑14:50 Decision Procedures
Chair: Alessandro Cimatti
Location: AT LT4
14:00 Min Zhou, Fei He, Bow-Yaw Wang and Ming Gu
On Array Theory of Bounded Elements

We investigate a first-order array theory of bounded elements. By reducing to the theory of weak second-order logic with one successor (WS1S), we show that the proposed array theory is decidable. Finally, two natural extensions to the new theory are shown to be undecidable.

14:25 David Monniaux
Quantifier elimination by lazy model enumeration

We propose a quantifier elimination scheme based on nested lazy model enumeration through SMT-solving, and projections. This scheme may be applied to any logic that fulfills certain conditions; we illustrate it for linear real arithmetic. The quantifier elimination problem for linear real arithmetic is doubly exponential in the worst case, and so is our method. We have implemented it and benchmarked it against other methods from the literature.

15:30‑17:10 Concurrent Program Verification II
Chair: Shaz Qadeer
Location: AT LT4
15:30 Pierre Ganty, Rupak Majumdar and Benjamin Monmege
Bounded Underapproximations

We show a new and constructive proof of the following language-theoretic result: for every context-free language L, there is a bounded context-free language L' included in L which has the same Parikh (commutative) image as L. Bounded languages, introduced by Ginsburg and Spanier, are subsets of regular languages of the form w1*w2*...wk* for some finite words w1,...,wk. In particular bounded subsets of context-free languages have nice structural and decidability properties. Our proof proceeds in two parts. First, using Newton's iterations on the language semiring, we construct a context-free subset Ls of L that can be represented as a sequence of substitutions on a linear language and has the same Parikh image as L. Second, we inductively construct a Parikh-equivalent bounded context-free subset of Ls.

As an application of this result in model checking, we show how to underapproximate the reachable state space of multithreaded procedural programs. The bounded language constructed above provides a decidable underapproximation for the original problem. By iterating the construction, we get a semi-algorithm for the original problems that constructs a sequence of underapproximations such that no two underapproximations of the sequence can be compared. This provides a progress guarantee: every word w in L is in some underapproximation of the sequence, and hence, a program bug is guaranteed to be found. In particular, we show that verification with bounded languages generalizes context-bounded reachability for multithreaded programs.

15:55 Anil Seth
Global Reachability in Bounded Phase Multi-Stack Pushdown Systems

Bounded phase multi-stack pushdown systems (mpds) have been studied recently. Given a set C of configurations of a mpds M, let pre*(M)(C,k) be the set of configurations of M from which M can reach an element of C in at most k phases. In this paper, we show that for any mpds M, any regular set C of configurations of M and any number k, the set pre*(M)(C,k) is regular. We use saturation like method to construct a non-deterministic finite multi-automaton recognizing pre*(M)(C,k). Size of the automaton constructed is double exponential in k which is optimal as worst case complexity measure.

16:20 Salvatore La Torre, P Madhusudan and Gennaro Parlato
Model-checking parameterized concurrent programs using linear interfaces

We consider the verification of parameterized Boolean programs--- abstractions of shared-memory concurrent programs with an unbounded number of threads. We propose that such programs can be model-checked by iteratively considering the program under $k$ round-robin schedules, for increasing values of $k$, using a novel concept called *linear interfaces*. Linear interfaces capture the input/output behavior of a *block* of concurrent threads in k rounds of interaction, and facilitate effective and symbolic algorithms for computing the reachable states in any k round-robin schedule. The restriction to k rounds of communication is an attractive under-approximation for finding bugs as most errors get manifest in only a few rounds. Analyzing parameterized programs by iteratively increasing the number of round-robin schedules, also paves the way to prove the *complete* correctness of the program (for any number of rounds and threads). We develop a game-theoretic algorithm that checks, soundly, whether k rounds of schedules are \emph{sufficient} to explore all reachable states, which allows us to declare a program entirely correct. We implement a symbolic model-checker using fixed-point equations, and report experiments on verifying parameterized programs obtained using predicate abstraction of Linux device drivers interacting with an operating system. We show that our techniques are effective in finding errors when they exist, as well as in proving parameterized drivers entirely correct.

16:45 Alexander Kaiser, Daniel Kroening and Thomas Wahl
Dynamic Cutoff Detection in Parameterized Concurrent Programs

The verification problem for parameterized concurrent programs is a grand challenge in computing. We consider the class of finite-state programs executed by an unbounded number of replicated threads, which is essential in concurrent software verification using predicate abstraction. While the reachability problem for this class is decidable, existing algorithms are of limited use in practice, due to an exponential-space lower bound. In this paper, we present an alternative method based on a reachability cutoff: a number n of threads that suffice to generate all reachable program locations. We give a sufficient condition, verifiable dynamically during the reachability analysis, that allows us to conclude that n is a cutoff. We then make the method complete, using a targeted backward coverability analysis. We demonstrate the efficiency of the approach on Petri net encodings of communication protocols, as well as on non-recursive Boolean programs run by arbitrarily many parallel threads.

17:10‑17:55 Tool Session
Chair: Kevin Jones
Location: AT LT4
17:10 Ernst Moritz Hahn, Holger Hermanns, Björn Wachter and Lijun Zhang
PARAM: A Model Checker for Parametric Markov Models

We present PARAM 1.0, a model checker for parametric discrete-time Markov chains (PMCs). PARAM can evaluate temporal properties of PMCs and certain extensions of this class. Due to parametricity, evaluation results are polynomials or rational functions. By instantiating the parameters in the result function, one can cheaply obtain results for multiple individual instantiations, based on only a single more expensive analysis. In addition, it is possible to postprocess the result function symbolically using for instance computer algebra packages, to derive optimum parameters or to identify worst cases.

17:25 Krishnendu Chatterjee, Thomas Henzinger, Barbara Jobstmann and Arjun Radhakrishna
GIST: A Solver for Probabilistic Games

Gist is a tool that (a) solves the qualitative analysis problem of turn-based probabilistic games with \omega-regular objectives; and (b)synthesizes reasonable environment assumptions for synthesis of unrealizable specifications. Our tool provides efficient implementations of several reduction based techniques to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic games to synthesize environment assumptions for unrealizable specifications.

17:40 Alessandro Ferrante, Maurizio Memoli, Margherita Napoli, Mimmo Parente and Francesco Sorrentino
A NuSMV Extension for Graded-CTL Model Checking

Graded-CTL is an extension of CTL with graded quantifiers allowing to reason about either "at least" or "all but" any number of possible futures. In this paper we show an extension of the NuSMV model-checker that includes an implementation of the symbolic algorithms for graded-CTL model checking. This implementation, based on the CuDD library for BDDs and ADDs manipulation, also includes an efficient algorithm for multiple counterexamples generation.