Abstract
The interplay back and forth between software model checking and hardware model checking has been fruitful for both. Originally intended for the analysis of concurrent software, model checking was first used in hardware verification. The abstraction methods developed for hardware verification however have been a stepping stone for the new generation of software verification tools including SLAM, BLAST, and MAGIC which focus on control-intensive software in C. Most recently, the experience with software verification is providing new leverage for verifying hardware designs in high level languages.
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
Ball, T., Rajamani, S.K.: Automatically Validating Temporal Safety Properties of Interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)
Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proc. 36th Conference on Design Automation (DAC), pp. 317–320 (1999)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 States and Beyond. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (1990)
Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular Verification of Software Components in C. In: Proc. 25th Int. Conference on Software Engineering (ICSE). pp. 385–395 (2003), Extended version in IEEE Transactions on Software Engineering, 2004
Clarke, E., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Clarke, E., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach. In: Proc. POPL, pp. 117–126 (1983)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000), Extended version in J. ACM 50(5): 752–794, 2003.
Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Clarke, E., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Clarke, E., Mishra, B.: Automatic Verification of Asynchronous Circuits. In: Proc. Logic of Programs, pp. 101–115 (1983)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. Symposium on Principles of Programming Languages (POPL), pp. 238–252 (1977)
Graf, S., Saidi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Proc. ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages, pp. 58–70 (2002)
Jain, H., Kroening, D., Clarke, E.: Verification of SpecC using predicate abstraction. In: MEMOCODE 2004, pp. 7–16. IEEE, Los Alamitos (2004)
Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994)
McMillan, K.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)
Pnueli, A.: The temporal logic of programs. In: Proc. 18th Symposium on Foundations of Computer Science (FOCS), pp. 46–67 (1977)
Queille, J., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Clarke, E., Gupta, A., Jain, H., Veith, H. (2008). Model Checking: Back and Forth between Hardware and Software. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)