{"id":287,"date":"2010-11-17T13:13:42","date_gmt":"2010-11-17T13:13:42","guid":{"rendered":"http:\/\/kglarkiv.cs.aau.dk\/?p=287"},"modified":"2011-02-04T17:46:44","modified_gmt":"2011-02-04T17:46:44","slug":"287","status":"publish","type":"post","link":"https:\/\/kglarkiv.cs.aau.dk\/?p=287","title":{"rendered":"Model Checking PhD course"},"content":{"rendered":"

.. by Doron Peled<\/a>, Bar Ilan University, Israel,\u00a0 Aalborg University
\nFebruary 7, 8 2011, Room 0.2.12, Selma Lagerl\u00f6fsvej 300, 9220 Aalborg.
\n<\/strong><\/span><\/p>\n

We are happy to (re)announce this short, but intense PhD course on the secrets of model checking, in particular for linear time and fairness properties, offered by one of the most prominent and productive researchers in the area.\u00a0 Amongst several books, together with Ed Clarke and Orna Grumberg,\u00a0 Doron Peled is the (co-) author of the authority book on the subject.<\/p>\n

\"\"<\/a>

Marktoberdorf 2010, Vicotory<\/p><\/div>\n

“Model Checking” is a generic name for methods for automatically checking the compatibility between a model and its formal specification. It is used to verify the correctness of software and hardware systems. The method has been successfully adopted by the hardware and software industry, and provides an automatic exhaustive alternative to software and hardware testing. Model checking usually compares a finite state model of a system (software or hardware against a specification given in some formal notation such as automata or logic.<\/p>\n

In this series of lectures we will learn the basic methods and algorithms for model checking and how to use them. We focus on the following topics:<\/p>\n