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

On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction
 by Vlad Rusu & Eli Singerman.

Lecture Notes in Computer Science, Volume 1579.
From Tools and Algorithms for the Construction and Analysis of Systems (TACAS '99).
Edited by W. Rance Cleaveland.
Springer-Verlag, Amsterdam, The Netherlands.
March, 1999.
Pages 178–192.


Abstract
We present a new approach for proving safety properties of reactive systems, based on tight interaction between static analysis, theorem proving and abstraction techniques. The method incrementally constructs a proof or finds a counterexample. Every step consists of applying one of the techniques and makes constructive use of information obtained from failures in previous steps. The amount of user intervention is limited and is highly guided by the system at each step. We demonstrate the method on three simple examples, and show that by using it one can prove more properties than by using each component as a stand-alone.
BibTEX Entry
@INPROCEEDINGS{Rusu&Singerman99,
    AUTHOR = {Vlad Rusu and Eli Singerman},
    TITLE = {On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction},
    VOLUME = {1579},
    YEAR = {1999},
    PAGES = {178--192},
    MONTH = {March},
    ADDRESS = {Amsterdam, The Netherlands},
    URL = {http://www.csl.sri.com/papers/tacas99/},
    SERIES = {Lecture Notes in Computer Science},
    BOOKTITLE = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS '99)},
    PUBLISHER = {Springer-Verlag},
    EDITOR = {{W.} Rance Cleaveland}
}
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