Model checking and abstraction
- 1 September 1994
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 16 (5) , 1512-1542
- https://doi.org/10.1145/186025.186051
Abstract
We describe a method for using abstraction to reduce the complexity of temporal-logic model checking. Using techniques similar to those involved in abstract interpretation, we construct an abstract model of a program without ever examining the corresponding unabstracted model. We show how this abstract model can be used to verify properties of the original program. We have implemented a system based on these techniques, and we demonstrate their practicality using a number of examples, including a program representing a pipelined ALU circuit with over 101300 states.Keywords
This publication has 10 references indexed in Scilit:
- Property preserving simulationsPublished by Springer Nature ,1993
- Model checking and modular verificationPublished by Springer Nature ,1991
- Tableau-based model checking in the propositional mu-calculusActa Informatica, 1990
- Trace Theory for Automatic Hierarchical Verification of Speed-Independent CircuitsPublished by MIT Press ,1989
- Automatic Verification of Sequential Circuits Using Temporal LogicIEEE Transactions on Computers, 1986
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986
- The complexity of propositional linear temporal logicsJournal of the ACM, 1985
- A denotational framework for data flow analysisActa Informatica, 1982
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967