SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

InVeSt : A Tool for the Verification of Invariants
 by Sam Owre, Saddek Bensalem & Yassine Lakhnech.

Abstract
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.
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy