On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction
- 12 March 1999
- book chapter
- Published by Springer Nature
- p. 178-192
- https://doi.org/10.1007/3-540-49059-0_13
Abstract
No abstract availableKeywords
This publication has 13 references indexed in Scilit:
- Symbolic model checking: 1020 States and beyondPublished by Elsevier ,2004
- Computing abstractions of infinite state systems compositionally and automaticallyPublished by Springer Nature ,1998
- Generating finite-state abstractions of reactive systems using decision proceduresPublished by Springer Nature ,1998
- Abstract interpretation of reactive systemsACM Transactions on Programming Languages and Systems, 1997
- Construction of abstract state graphs with PVSPublished by Springer Nature ,1997
- Symbolic model checking of infinite state systems using presburger arithmeticPublished by Springer Nature ,1997
- Verification of Real-Time Systems using Linear Relation AnalysisFormal Methods in System Design, 1997
- Verifying invariants using theorem provingPublished by Springer Nature ,1996
- Experiments in theorem proving and model checking for protocol verificationPublished by Springer Nature ,1996
- Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpointsPublished by Association for Computing Machinery (ACM) ,1977