Distributed and Complex Systems Group : Homepage

:Vérimag Distributed and Complex Systems Group

Program Verification

News

  • The paper "Quantitative Separation Logic and Programs with Lists" by Radu Iosif, Marius Bozga and Swann Perarnau has been accepted to IJCAR 2008.  (new)
  • The paper "What else is decidable about integer arrays" by Peter Habermehl (LSV), Radu Iosif (Verimag) and Tomas Vojnar (Brno University of Technology) has been accepted to FOSSACS 2008.  (new)

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.