%0 Conference Proceedings
%F rzc02
%A Rusu, V.
%A Zinovieva, E.
%A Clarke, D.
%T Verifying Invariants More Automatically
%B Verification and Computatoiional Logic, VCL'02
%X We present an algorithm that, given a transition system S and a set of auxiliary invariants A already proved on S, checks if a predicate I is inductive on S in the context of the auxiliary invariants. The answer is either yes, in which case I is an invariant of S, or don't know. The algorithm accepts infinite-state systems with unbounded counters and parametric-size arrays, and predicates with quantifiers over unbounded domains. As an example we verify a component of an electronic purse system. By using our algorithm together with the PVS theorem prover the verification is more automatic than that performed using PVS alone
%U http://www.irisa.fr/vertecs/Equipe/Rusu/VCL02/
%D 2002