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

A Technique for Invariant Generation
 by Dr. Harald Rue▀, Dr. Hassen Sa´di, Dr. Natarajan Shankar & Dr. Ashish Tiwari.

Lecture Notes in Computer Science, Volume 2031.
From TACAS 2001 - Tools and Algorithms for the Construction and Analysis of Systems.
Edited by Tiziana Margaria and Wang Yi.
Springer-Verlag, Genova, Italy.
April, 2001.
Pages 113–127.


Abstract
Most of the properties established during verification are either invariants or depend crucially on invariants. The effectiveness of automated formal verification is therefore sensitive to the ease with which invariants, even trivial ones, can be automatically deduced. While the strongest invariant can be defined as the least fixed point of the strongest post-condition of a transition system starting with the set of initial states, this symbolic computation rarely converges. We present a method for invariant generation that relies on the simultaneous construction of least and greatest fixed points, restricted widening and narrowing, and quantifier elimination. The effectiveness of the method is demonstrated on a number of examples.
BibTEX Entry
@inproceedings{TRSS:TACAS01,
    AUTHOR = {{A.} Tiwari and {H.} Rue\ss and {H.} Sa\"{i}di and {N.} Shankar},
    TITLE = {{A} Technique for Invariant Generation},
    BOOKTITLE = {{TACAS} 2001 - Tools and Algorithms for the Construction and Analysis of Systems},
    YEAR = {2001},
    EDITOR = {Tiziana Margaria and Wang Yi},
    SERIES = {Lecture Notes in Computer Science},
    VOLUME = {2031},
    PAGES = {113--127},
    ADDRESS = {Genova, Italy},
    MONTH = {apr},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/tacas01/}
}
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