%0 Conference Paper %1 Pnueli01automaticdeductive %A Pnueli, Amir %A Ruah, Sitvanit %A Zuck, Lenore %B TACAS %D 2001 %I Springer %K German automated cutoff deductive finite_state invariant_discovery modelchecking parameterized verification %P 82-97 %T Automatic Deductive Verification with Invisible Invariants %U http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.524 %X The paper presents a method for the automatic verification of a certain class of parameterized systems. These are bounded-data systems consisting of N processes (N being the parameter), where each process is finite-state. First, we show that if we use the standard deductive inv rule for proving invariance properties, then all the generated verification conditions can be automatically resolved by finite-state (bdd-based) methods with no need for interactive theorem proving. Next, we show how to use model-checking techniques over finite (and small) instances of the parameterized system in order to derive candidates for invariant assertions. Combining this automatic computation of invariants with the previously mentioned resolution of the VCs (verification conditions) yields a (necessarily) incomplete but fully automatic sound method for verifying boundeddata parameterized systems. The generated invariants can be transferred to the VC-validation phase without ever been examined by the user, which explains why we refer to them as "invisible". We illustrate the method on a non-trivial example of a cache protocol, provided by Steve German.

@inproceedings{Pnueli01automaticdeductive, abstract = {The paper presents a method for the automatic verification of a certain class of parameterized systems. These are bounded-data systems consisting of N processes (N being the parameter), where each process is finite-state. First, we show that if we use the standard deductive inv rule for proving invariance properties, then all the generated verification conditions can be automatically resolved by finite-state (bdd-based) methods with no need for interactive theorem proving. Next, we show how to use model-checking techniques over finite (and small) instances of the parameterized system in order to derive candidates for invariant assertions. Combining this automatic computation of invariants with the previously mentioned resolution of the VCs (verification conditions) yields a (necessarily) incomplete but fully automatic sound method for verifying boundeddata parameterized systems. The generated invariants can be transferred to the VC-validation phase without ever been examined by the user, which explains why we refer to them as "invisible". We illustrate the method on a non-trivial example of a cache protocol, provided by Steve German.}, added-at = {2010-01-28T10:36:09.000+0100}, author = {Pnueli, Amir and Ruah, Sitvanit and Zuck, Lenore}, biburl = {https://www.bibsonomy.org/bibtex/243613d946ff2174a93f069426269d075/giuliano.losa}, booktitle = {TACAS}, description = {Automatic Deductive Verification with Invisible Invariants}, interhash = {5a6793471f9fe3ca1d3eeed5bc20c4a4}, intrahash = {43613d946ff2174a93f069426269d075}, keywords = {German automated cutoff deductive finite_state invariant_discovery modelchecking parameterized verification}, pages = {82-97}, publisher = {Springer}, timestamp = {2010-01-28T10:36:09.000+0100}, title = {Automatic Deductive Verification with Invisible Invariants}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.524}, year = 2001 }