The Invariant Checker - Publications

# Invariant Checker and predicate abstraction - Publications

[BGL03] Abstraction as the Key for Invariant Verification
Saddek Bensalem, Susanne Graf, Yassine Lakhnech

In Int. Symposium on Verification celebrating Zohar Manna's 64th Birthday , LNCS 2772, Springer Verlag 2003

Abstract
We present a methodology for constructing abstractions and refining them by analyzing counter-examples. We also present a uniform verification method that combines abstraction, model-checking and deductive verification. In particular, we show how to use the abstract system in a deductive proof even when the abstract model does not satisfy the specification but simulates the concrete system with respect to a weaker notion of simulation than Milner's.

PDF

[Sai98] Combinaison de Methodes Deductives et Algorithmiques pour la Verication
Hassen Saidi

In PhD thesis, obtained from Universite Joseph Fourier - Grenoble I, January 27, 1998 in Grenoble

Abstract
to come

PDF

[GS97] Construction of abstract state graphs with PVS
Susanne Graf and Hassen Saidi

In Proceedings of the 9th Conference on Computer-Aided Verification (CAV'97), Haifa, Israel, June 1997.

Abstract
In this paper, we propose a method for the automatic construction of an abstract state graph of an arbitrary system using the PVS theorem prover. Given a parallel composition of sequential processes and predicates $p_1 ... p_n$ on the program variables defining an abstract domain, we construct an abstract state graph, starting in the state defined by the values of the predicates $p_1 ... p_n$ in the initial state. The possible successors of a state are computed using the PVS theorem prover by verifying for each $p_i$ if $p_i$ or $\neg p_i$ is a postcondition of it. This allows an abstract state space exploration for arbitrary programs. Using this method, we have automatically verified a bounded retransmission protocol which cannot be proved using backward analysis without providing strong auxiliary invariants.

PDF

[Sai97] The Invariant-Checker : Automated Deductive Verification of Reactive Systems
Hassen Saidi

In The Invariant-Checker : Automated Deductive Verification of Reactive Systems , Haifa, Israel, June 1997.

Abstract
Tool Presentation. The Invariant Checker is a tool for the computer aided verification, dedicated to the proof of invariance properties of reactive systems. The aim of the tool is to provide a framework combining theorem-proving techniques (PVS theorem prover) and deductive verification methods. Systems are described as a parallel composition of sequential programs described in a language close to the Dijkstra's guarded command language. Program variables can be of any type definable in PVS. The tool provides automatic generation of invariants, automatic strengthening of invariants and automatic abstraction. The tool is interfaced with Ald\'ebaran, a tool for the analysis of state graphs.

not available

[LS97] Automatic Verification of Parameterized Networks of Processes by Abstraction
David Lesens and Hassen Saidi

In Proceedings of the 2nd International Workshop on the Verification of Infinite State Systems (INFINITY'97) , Bologna, Italy, July 1997 (appeared in ENTCS)

Abstract
In this paper we are interested in the verification of safety properties of parameterized networks. A network is defined as a parallel composition of an arbitrary but finite number of identical sequential processes, where we consider parallel composition by interleaving and synchronization by shared variables. Using abstraction techniques, a process, called an {\it abstract network}, encoding the behavior of the entire network is constructed. The property is then checked on this process. Our verification method has the following advantages: the construction of the abstract network is fully automatic; the obtained process is generally a simple process on which the property can be easily verified. Of course, if the property cannot be verified on the abstract network, another weaker abstraction has to be computed. The construction requires to discharge a set of first order verification conditions (VCs). The PVS theorem prover is used to discharge the generated VCs. This allows us to consider processes with arbitrary data types. The effectiveness of our verification method is illustrated on two examples including a parameterized version of the Fischer's protocol.

experimental results (no more available)

[GS96] Verifying Invariants Using Theorem Proving
Susanne Graf and Hassen Saidi

In Proceedings of 8th Computer-Aided Verification, July 1996, New Brunswick, NJ. LNCS, Springer-Verlag.

Abstract
We are interested in using a theorem prover in order to verify invariance properties of systems in a systematic model checking like'' manner. A system is described as a set of sequential components, each one given by a transition relation and a predicate Init defining the set of initial states. In order to verify that P is an invariant of system S, we try to compute, in an iterative model checking like manner, a predicate P' stronger than P and weaker than Init which is an inductive invariant, that is, whenever P' is true in some state , then P' remains true after the execution of any possible transition. The fact that P' is inductive can be expressed by a set of predicates (having no more quantifiers than P) on the set of program variables, one for every possible transition of the system. In order to prove that P' is inductive, we use either automatic or assisted theorem proving depending on the nature of the formulas to prove. We show in this paper how this can be done in an efficient way. The prover we use is the Prototype Verification System PVS. A tool implementing this verification method is presented.

[BLS96] Powerful Techniques for the Automatic Generation of Invariants
Saddek Bensalem, Yassine Lakhnech, Hassen Saidi

In Proceedings of 8th Computer-Aided Verification , July 1996, New Brunswick, NJ. LNCS, Springer-Verlag.

Abstract
When proving invariance properties of programs one is faced with two problems. The first problem is related to the necessity of proving tautologies of the considered assertion language, whereas the second manifests in the need of finding sufficiently strong invariants. This paper focuses on the second problem and describes techniques for the automatic generation of invariants. The first set of these techniques is applicable on sequential transition systems and allows to derive so-called local invariants, i.e. predicates which are invariant at some control location. The second is applicable on networks of transition systems and allows to combine local invariants of the sequential components to obtain local invariants of the global systems. Furthermore, a refined strengthening technique is presented that allows to avoid the problem of size-increase of the considered predicates which is the main drawback of the usual strengthening technique. The proposed techniques are illustrated by examples.

Gzipped Postscript

[LGBBS95] Property Preserving Abstractions for the Verification of Concurrent Systems
C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, S. Bensalem

In Formal Methods in System Design , Vol 6, Iss 1, January 1995

Abstract
We study property preserving transformations for reactive systems. The main idea is the use of simulations parameterized by Galois connections (alpha,gamma), relating the lattices of properties of two systems. We propose and study a notion of preservation of properties expressed by formulas of a logic, by a function alpha mapping sets of states of a system S into sets of states of a system S'. Roughly speaking, alpha preserves f if the satisfaction of f at some state of S implies that f is satisfied by any state in the image of this state by alpha. We give results on the preservation of properties expressed in sublanguages of the branching time mu-calculus when two systems S and S' are related via (alpha,gamma)-simulations. They can be used in particular to verify a property for a system by proving this property on a simpler system which is an abstraction of it. We show also under which conditions abstraction of concurrent systems can be computed from the abstraction of their components. This allows a compositional application of the proposed verification method. This is a revised version of the papers that appeared in CAV'92 [BensalemBouajjaniLoiseauxSifakis92] and in TAPSOFT'93 [GrafLoiseaux92]; the results are fully developed in the thesis of Claire Loiseaux (in french).

PDF

[GL93] Program Verification using compositional Abstraction
S. Graf, C. Loiseaux

In TAPSOFT 93, joint conference CAAP/FASE ,LNCS 668, Springer Verlag

Abstract
In this paper we describe a method for the obtention of the minimal transition system, representing a communicating system given by a set of parallel processes, avoiding the complexity of the non minimal transition system. We consider minimization with respect to observational equivalence, but the method may be adapted to any other equivalence. An interesting method to achieve this goal is to proceed by stepwise composition and minimization of the components of the system. However, if no precautions are taken, the intermediate state graphs generated by this method may contain a lot of transitions which are impossible in the whole context. We give here a variant of this method which allows to avoid these impossible transitions by taking into account at each composition step a guess of the interface behaviour of the context. This interface specification'' must be provided by the user. The method is based on a reduction operator for the composition of a subsystem with its interface specification, which is similar to the parallel operator but introduces undefinedness predicates whereever the interface cuts off'' a transition. The parallel operator is defined in a way that these undefinedness predicates disappear again in the full context if and only if the corresponding transition is in fact impossible in the whole system. The efficiency of the method depends in fact on the accuracy with which the designer is able to approximate the possible sequences of the context, but its correctness does not. The proof of the correctness of the method is based on a preorder relation similar to the one defined by Walker.

PDF