**[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.

** [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

** [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.

** [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.

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.

** [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)

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.

**[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).

**[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.