InVeSt swMATH ID: 12034 Software Authors: Bensalem S, Lakhnech Y, Owre S Description: 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 [15]. 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. Homepage: http://link.springer.com/chapter/10.1007/BFb0028771 Related Software: PVS; TREX; HOL; ACL2; HyTech; SPIN; MiniSat; MDGs; Uppaal; ML; Bandera; Omega; UNITY; D-Finder; MOCHA; SLAM; Kronos; CADP; SMV; REDUCE Cited in: 10 Publications all top 5 Cited by 24 Authors 3 Bensalem, Saddek 3 Bouajjani, Ahmed 2 Abdulla, Parosh Aziz 2 Annichini, Aurore 2 Lakhnech, Yassine 1 Abed, Sa’ed 1 Aït Mohamed, Otmane 1 Bharadwaj, Ramesh 1 Bozga, Marius 1 Collomb-Annichini, Aurore 1 Contensin, Magali 1 Das, Satyaki 1 Dill, David L. 1 Graf, Susanne 1 Habermehl, Peter 1 Jonsson, Bengt 1 Nguyen, Thanh-Hung 1 Pierre, Laurence 1 Rybina, Tatiana 1 Sammane, Ghiath Al 1 Sifakis, Joseph 1 Sighireanu, Mihaela 1 Sims, Steve 1 Voronkov, Andrei Cited in 2 Serials 1 Formal Aspects of Computing 1 Formal Methods in System Design Cited in 2 Fields 10 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) Citations by Year