HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

Interactive Abstractions: Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction

Vlad Rusu 1 Eli Singerman 2
1 PAMPA - Models and Tools for Programming Distributed Parallel Architectures
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
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 some examples and show that by using it one can prove more properties than by using each component as a stand-alone.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00072938
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 11:19:50 AM
Last modification on : Friday, February 4, 2022 - 3:25:09 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:28:41 PM

Identifiers

  • HAL Id : inria-00072938, version 1

Citation

Vlad Rusu, Eli Singerman. Interactive Abstractions: Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction. [Research Report] RR-3726, INRIA. 1999. ⟨inria-00072938⟩

Share

Metrics

Record views

89

Files downloads

138