Edmund M. Clarke , 
E. Allen Emerson , 
Joseph Sifakis Authors Info & ClaimsAuthors : Edmund M. Clarke , E. Allen Emerson , Joseph Sifakis Authors Info & Claims
This alert has been successfully added and will be sent to: You will be notified whenever a record that you have chosen has been cited.
To manage your alert preferences, click on the button below. Manage my AlertsIn 1981, Edmund M. Clarke and E. Allen Emerson, working in the USA, and Joseph Sifakis working independently in France, authored seminal papers that founded what has become the highly successful field of model checking. This verification technology provides an algorithmic means of determining whether an abstract model---representing, for example, a hardware or software design---satisfies a formal specification expressed as a temporal logic (TL) formula. Moreover, if the property does not hold, the method identifies a counterexample execution that shows the source of the problem.
The progression of model checking to the point where it can be successfully used for complex systems has required the development of sophisticated means of coping with what is known as the state explosion problem. Great strides have been made on this problem over the past 28 years by what is now a very large international research community. As a result many major hardware and software companies are beginning to use model checking in practice. Examples of its use include the verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms.
The work of Clarke, Emerson, and Sifakis continues to be central to the success of this research area. Their work over the years has led to the creation of new logics for specification, new verification algorithms, and surprising theoretical results. Model checking tools, created by both academic and industrial teams, have resulted in an entirely novel approach to verification and test case generation. This approach, for example, often enables engineers in the electronics industry to design complex systems with considerable assurance regarding the correctness of their initial designs. Model checking promises to have an even greater impact on the hardware and software industries in the future.
---Moshe Y. Vardi, Editor-in-ChiefBall, T., Rajamani, S.K. The SLAM toolkit. In Computer-Aided Verification (CAV'01). Volume 2102 of Lecture Notes in Computer Science (2001), 260--264.
Basu, A., Bozga, M., Sifakis, J. Modeling heterogeneous real-time components in BIP. In SEFM (2006), 3--12.
Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D. Uppaal-tiga: Time for playing games! In CAV. W. Damm and H. Hermanns, eds. Volume 4590 of Lecture Notes in Computer Science (Springer, 2007), 121--125.
Ben-Ari, M., Pnueli, A., Manna, Z. The temporal logic of branching time. Acta Inf. 20 (1983), 207--226.
Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J. D-finder: A tool for compositional deadlock detection and verification. In CAV. A. Bouajjani and O. Maler, eds. Volume 5643 of Lecture Notes in Computer Science (Springer, 2009), 614--619.
Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.-H. Compositional verification for component-based systems and application. In ATVA. S.-D. Cha, J.-Y. Choi, M. Kim, I. Lee, and M. Viswanathan, eds. Volume 5311 of Lecture Notes in Computer Science (Springer, 2008), 64--79.
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y. Symbolic model checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'99). R. Cleaveland, ed. Volume 1579 of Lecture Notes in Computer Science (Springer-Verlag, Mar. 1999), 193--207.
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J. Symbolic Model Checking: 10 20 states and beyond. Inf. Comput. 98, 2 (June 1992), 142--170. Originally presented at the 1990 Symposium on Logic in Computer Science (LICS'90).
