%0 Conference Proceedings
%F r01a
%A Rusu, V.
%T Verifying that Invariants are Context-Inductive
%B Theorem Proving in Higher-Order Logics (TPHOLs'01),, Category B paper, University of Edinburgh research Report EDI-INF-RR-0046
%P 337-351
%X We study the deductive verification of infinite-state systems modeled by extended automata. Typically, this process requires proving many invariants, and automatically discharging these proof obligations would save the user a significant amount of effort. To accomplish this we present techniques for automatically verifying that invariants are inductive in a given context, and identify a class of systems and a logic for expressing invariants and contexts for which the problem is decidable
%U http://www.irisa.fr/vertecs/Publis/Ps/2001-TPHOL.ps.gz
%D 2001