Difference between revisions of "EECI 2012: Model Checking and Logic Synthesis"

From MurrayWiki
Jump to: navigation, search
(Created page with '{{righttoc}} This lecture provides an introduction to automata based model checking. We first describe how automata based model checking works, including an efficient algorithm …')
 
Line 4: Line 4:
  
 
==  Lecture Materials ==
 
==  Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/eeci2011/L4_model_checking-21Mar11.pdf Model Checking with Spin] (Presentation and notation follow that in "Model Checking" chapter 5.2 by Baier and Katoen and "The SPIN Model Checker: Primer and Reference Manual" by Holzmann.)
+
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/AFRL12/L4_Model_Checking_Logic_Synthesis.pdf Model Checking and Logic Synthesis] (Presentation and notation follow that in "Model Checking" chapter 5.2 by Baier and Katoen.)
  
 
== Further Reading ==
 
== Further Reading ==

Revision as of 00:28, 22 April 2012

This lecture provides an introduction to automata based model checking. We first describe how automata based model checking works, including an efficient algorithm for computing language intersection. The rest of the lecture focuses on the use of Spin model checker and the computational complexity issue.

Lecture Materials

Further Reading

  • The SPIN Model Checker: Primer and Reference Manual, G. J. Holzmann, Addison-Wesley Professional, 2003. A comprehensive reference on Spin model checker

  • Principles of Model Checking, C. Baier and J.-P. Katoen, The MIT Press, 2008. A detailed reference on model checking. Slides for this lecture follow Chapter 6 of this reference.

  • Model Checking, E. M. Clarke, O. Grumberg and D. A. Peled, The MIT Press, 1999. A very good reference on automata based model checking.

Additional Information