Model Checking @CMU
[Home]

[People]

[Software]

[Publications]

[Support]

 [Links]

[Internal]

 

 

 Model Checking Publications

This page presents papers on model checking written by project members. Some of these papers are available in postscript format. The others can be obtained by contacting Ed Clarke.

Copies of most papers will be available through this page soon. In the mean time, please contact Ed Clarke for copies.

  • Surveys
  • Explicit state model checking
  • Symbolic model checking
  • Real-time extensions
  • Model Checking for Security
  • Model Checking for Hybrid Systems
  • Selected publications online

    • Surveys

  • E. Clarke, O. Grumberg and D. Long. Verification tools for finite-state concurrent systems. In: A Decade of Concurrency - Reflections and Perspectives. Lecture Notes in Computer Science, 803, 1994.

    • Explicit state model checking

  • 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 Lecture Notes in Computer Science, volume 131. Springer-Verlag, 1981

  • E. M. Clarke, E. A. Emerson and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. In ACM Transactions on Programming Languages and Systems, 8(2):244--263, 1986.

    • Symbolic model checking

  • J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In VLSI 91, Edinburgh, Scotland, 1990.

  • J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In 27th ACM/IEEE Design Automation Conference, 1990.

  • J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 10E20 states and beyond. In LICS, 1990.

  • K. L. McMillan. Symbolic model checking - an approach to the state explosion problem. PhD thesis, SCS, Carnegie Mellon University, 1992.

  • 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, Proceedings of the Eleventh 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.

    • Real-time extensions

  • S. Campos and E. Clarke, Real-time symbolic model checking for discrete time models. In AMAST Series in Computing: Theories and Experiences for Real-Time System Development. T. Rus, C. Rattray, editors. World Scientific Publishing Company, 1995.

  • S. Campos, E. Clarke, W. Marrero and M. Minea, Verus: a tool for quantitative analysis of finite-state real-time systems. In: Workshop on Languages, Compilers and Tools for Real-Time Systems, 1995.

  • S. Campos, E. Clarke, W. Marrero and M. Minea, Timing analysis of industrial real-time systems. In Workshop on Industrial Strength Formal Specification Techniques, 1995.

  • S. Campos, E. Clarke, W. Marrero, M. Minea and H. Hiraishi, Computing quantitative characteristics of finite-state real-time systems. In IEEE Real-Time Systems Symposium, 1994.

  • S. Campos, The priority inversion problem and real-time symbolic model checking. Technical Report CMU-SCS-93-125, Carnegie Mellon University, 1993.

    • Model Checking for Security

  • W. Marrero, E.M. Clarke, and S. Jha. Model Checking for Security Protocols. Technical Report CMU-SCS-97-139, Carnegie Mellon University, May 1997.

  • E.M. Clarke, and S. Jha, W. Marrero. Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In Proceedings of the IFIP Working Conference on Programming Concepts and Methods (PROCOMET), 1998.

  • E.M. Clarke, and S. Jha, W. Marrero. A machine checkable logic of knowledge for specifying security properties of electronic commerce protocols. LICS Security Workshop, 1998.

    • Model Checking for Hybrid Systems

  • J. Kapinski, A. Donze, F. Lerda, H. Maka, E. M. Clarke, and B. H. Krogh. Model Checking Control Software for Nonlinear Dynamic Systems. Extended abstract submitted to invited sessions of the 2008 Guidance, Navigation, and Control Conference.

  • F. Lerda, J. Kapinski, E. M. Clarke, and B. H. Krogh. Verification of Supervisory Control Software Using State Proximity and Merging. To appear in the 11th International Conference on Hybrid Systems: Computation and Control, 2008.

  • F. Lerda, J. Kapinski, H. Maka, E. M. Clarke, and B. H. Krogh. Model Checking In-The-Loop. To appear in the proceedings of the 2008 American Control Conference.

    • Related papers

  • R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.

    • Selected publications online

      CMU-SCS Model Checking home page

    Please send any comments and suggestions to  Nishant Sinha - (nishants) at cs dot cmu dot edu.