Model Checking
Authors:
- Edmund M. ClarkeECEdmund M. Clarke
- Bernd-Holger SchlingloffBSBernd-Holger Schlingloff
- 1 January 2001
- book chapter
- Published by Elsevier
- p. 1635-1790
Abstract
No abstract availableThis publication has 61 references indexed in Scilit:
- Symbolic Boolean manipulation with ordered binary-decision diagramsACM Computing Surveys, 1992
- On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplicationIEEE Transactions on Computers, 1991
- Circuit width, register allocation, and ordered binary decision diagramsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1991
- Reasoning about networks with many identical finite state processesInformation and Computation, 1989
- Characterizing finite Kripke structures in propositional temporal logicTheoretical Computer Science, 1988
- Monotone versus positiveJournal of the ACM, 1987
- Automatic Verification of Sequential Circuits Using Temporal LogicIEEE Transactions on Computers, 1986
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- Defining livenessInformation Processing Letters, 1985
- The temporal logic of branching timeActa Informatica, 1983