Abstract
Symbolic model checking is a powerful formal specification and verification method that has been applied successfully in several industrial designs. Using symbolic model checking techniques it is possible to verify industrial-size finite state systems. State spaces with up to 1030 states can be exhaustively searched in minutes. Models with more than 10120 states have been verified using special techniques.
Several extensions to the original technique have been developed, making it even more powerful. Timing properties can be verified by performing a quantitative timing analysis [3, 5]. The designer can then analyze the performance of a system and gain insight in how well a system works early in the design process. Word-level model checking allows the verification of datapaths in addition to control [12]. Symmetry [8], abstraction [10, 15] and compositional reasoning [15] techniques significantly extend the power of model checking by exploiting the hierarchical structure of complex circuit designs and protocols.
More information about SMV, as well as the source code for the model checker can be found at: http://www.cs.cmu.edu/∼modelcheck
This research was sponsored in part by the National Science Foundation under grant no. CCR-8722633, by the Semiconductor Research Corporation under contract 92-DJ-294, and by The Defense Advanced Research Projects Agency, Information Science and Technology Office, under the title “Research on Parallel Computing”, ARPA Order No. 7330, issued by DARPA/CMO under Contract MDA972-90-C-0035.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Symposium on Logic in Computer Science, 1990.
S. Campos, E. Clarke, W. Marrero, and M. Minea. Verifying the performance of the PCI local bus using symbolic techniques. In International Conference on Computer Design, 1995.
S. V. Campos, E. M. Clarke, W. Marrero, and M. Minea. Timing analysis of industrial realtime systems. In Workshop on Industrial-strength Formal specification Techniques, 1995.
S. V. Campos, E. M. Clarke, W. Marrero, M. Minea, and H. Hiraishi. Computing quantitative characteristics of finite-state real-time systems. In IEEE Real-Time Systems Symposium, 1994.
E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs: Workshop, Yorktown Heights, NY, May 1981. Springer-Verlag, 1981, Lecture Notes in Computer Science, volume 131.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
E. M. Clarke, T. Filkorn, and S. Jha. Exploiting symmetry in temporal logic model checking. In Proceedings of the Fifth Workshop on Computer-Aided Verification, June 1994.
E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, and L. A. Ness. Verification of the Futurebus+cache coherence protocol. In L. Claesen, editor, International Symposium on Computer Hardware Description Languages and their Applications. North-Holland, April 1993.
E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. In Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages, January 1992.
E. M. Clarke, O. Grumberg, and D. E. Long. Verification tools for finite-state concurrent systems. In A Decade of Concurrency — Reflections and Perspectives, 1994. Springer Lecture Notes in Computer Science, 803.
E. M. Clarke, M. Khaira, and X. Zhao. Word level model checking — avoiding the pentium FDIV error. In Design Automation Conference, June 1996.
V. Hartonas-Garmhausen, E.M. Clarke, and S. Campos. Deadlock prevention in flexible manufacturing systems using symbolic model checking. In International Conference on Robotics and Automation, 1996.
V. Hartonas-Garmhausen, T. Kurfess, E.M. Clarke, and D. Long. Automatic verification of industrial designs. In Workshop on Industrial-strength Formal specification Techniques, 1995.
D. E. Long. Model checking, abstraction and compositional reasoning. PhD thesis, SCS, Carnegie Mellon University, 1993.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Clarke, E., McMillan, K., Campos, S., Hartonas-Garmhausen, V. (1996). Symbolic model checking. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_93
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_93
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive