InVeSt: a tool for the verification of invariants. A very important class of properties of reactive systems consists of invariance properties which state that all reachable states of the considered system satisfy some given property. Indeed, every safety property can be reduced to an invariance property and to prove progress properties one needs to establish invariance properties . Proving invariance properties is especially crucial for infinite and large finite state systems which escape algorithmic methods. In this paper we present the tool In VeSt which supports the verification of invariance properties of infinite state systems. In VeSt integrates deductive and algorithmic verification principles for the verification of invariance properties as well as abstraction techniques.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Abed, Sa’ed; Mohamed, Otmane Ait; Al Sammane, Ghiath: Automatic verification of reduction techniques in higher order logic (2013)
- Bensalem, Saddek; Bozga, Marius; Sifakis, Joseph; Nguyen, Thanh-Hung: Compositional verification for component-based systems and application (2008)
- Abdulla, Parosh Aziz; Collomb-Annichini, Aurore; Bouajjani, Ahmed; Jonsson, Bengt: Using forward reachability analysis for verification of lossy channel systems (2004)
- Bensalem, Saddek; Graf, Susanne; Lakhnech, Yassine: Abstraction as the key for invariant verification (2003)
- Das, Satyaki; Dill, David L.: Counter-example based predicate discovery in predicate abstraction (2002)
- Rybina, Tatiana; Voronkov, Andrei: Using canonical representations of solutions to speed up infinite-state model checking (2002)
- Annichini, Aurore; Bouajjani, Ahmed; Sighireanu, Mihaela: TREX: A tool for reachability analysis of complex systems (2001)
- Bharadwaj, Ramesh; Sims, Steve: Salsa: Combining constraint solvers with BDDs for automatic invariant checking (2000)
- Abdulla, Parosh Aziz; Annichini, Aurore; Bensalem, Saddek; Bouajjani, Ahmed; Habermehl, Peter; Lachnech, Yassine: Verification of infinite-state systems by combining abstraction and reachability analysis (1999)