A bit of history
The idea of predicate abstraction originates in the CAV’97 paper of Graf and Saidi Construction of abstract state graphs with PVS.This technique has led to actual cutting-edge program verification tools, such as SLAM or BLAST. Using abstraction for automatic invariant generation has been initiated in the CAV’96 paper Powerful Techniques for the Automatic Generation of Invariants by Bensalem, Lakhnech, and Saidi. This led to a tool called INVEST, which also implements the technique of counterexample-guided abstraction refinement (CEGAR). More information can be found in: S. Bensalem and Y. Lakhnech. Automatic Generation of Invariants. Formal Methods in System Design 15(1), 1999.
On a different line of work, the idea of using finite transducers to over-approximate the semantics of a program has been contributed to by the CAV’01 paper by Dams, Lakhnech and Steffen Iterating Transducers. Identifying systems with infinite but regular state spaces has been, among others, introduced in: Abstracting WS1S Systems to Verify Prameterized Networks K. Baukus, S. Bensalem, Y. Lakhnech, and K. Stahl (TACAS’00). Eventually, this led to the framework of regular model checking which is, together with predicate abstraction and static analysis, one of the most promising approaches for verifying software. Recent developments
Developing program verification techniques that can be applied to real-life software has made keen researchers from both static analysis and model checking communities. However, the major obstacles that hinder the application of existing verification techniques to software are due to the complexity of the data structures used in most industrial-scale programming languages (C, C++, Java). Our research focuses on programs handling dynamic lists, trees, and arrays with integer data. In contrast with existing work, we identify decidable classes of programs, for which verification of different properties (e.g. safety, termination) is possible automatically. For the programs falling outside the decidable classes, we use either approximate (e.g. widening) or semi-algorithmic (e.g. acceleration) techniques.
- The verification of programs handling singly-linked lists is directly amenable to the verification of counter automata, for which dedicated tools (e.g. ARMC, FAST or ASPIC) can be used. This method is implemented in the L2CA tool. More details can be found in:
— A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro and T. Vojnar. Programs with Lists are Counter Automata (CAV 2006) VERIMAG TR-2006-3
— M. Bozga and R. Iosif. On Flat Programs with Lists (VMCAI 2007) VERIMAG TR-2006-5
— M. Bozga, R. Iosif and S. Perarnau. Quantitative Separation Logic and Programs with Lists. VERIMAG TR-2007-9 - Programs handling doubly-linked lists, trees and trees with regular pointers (e.g. trees with parent pointers, root pointers, or trees in which all leaves are kept in a list) are dealt with using tree automata as over-approximations of sets of reachable configurations. This technique is implemented in the ARTMC tool. More details can be found in:
— A. Bouajjani, P. Habermehl, A. Rogalewicz and T. Vojnar. Abstract Regular Tree Model Checking of Complex Dynamic Data Structures (SAS 2006)
— P. Habermehl, R.Iosif, A. Rogalewicz and T. Vojnar. Proving Termination of Tree Manipulating Programs (ATVA 2007) VERIMAG TR-2007-1 - We have recently addressed the verification of programs with integer arrays using a new decidable logic for arrays. More details can be found in:
— P. Habermehl, R. Iosif and T. Vojnar. What else is decidable about integer arrays? (FOSSACS 2008) - Counter automata are central to the verification techniques we deploy. An important decidable class is called flat counter automata. We have implemented a library, called FLATA, for building and analyzing such models. More details can be found in:
— M. Bozga, R. Iosif and Y. Lakhnech. Flat Parametric Counter Automata (ICALP 2006) VERIMAG TR 2005-15
— M. Bozga, R. Iosif and V. Sfyrla. An Efficient Algorithm for the Computation of Optimum Paths in Weighted Graphs (MEMICS 2007)
CNRS
