.. by Doron Peled, Bar Ilan University, Israel, Aalborg University February 7, 8 2011, Room 0.2.12, Selma Lagerlöfsvej 300, 9220 Aalborg.
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. Amongst several books, together with Ed Clarke and Orna Grumberg, Doron Peled is the (co-) author of the authority book on the subject.
Marktoberdorf 2010, Vicotory
“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.
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:
Modeling of software and hardware systems.
Software specification using temporal logic and Büchi Automata.
Translation between logic and automata.
Model Checking Algorithms.
Specification and usage of fairness properties
How to make it work in practice: abstraction/reduction/BDDs
Time, Venue, ECTS, … :
Monday January 7 and Tuesday January 8, 2011 (note new dates) Room 0.2.12.
2 ECTS. A successful completion of the course consists in participation of the 2 days lectures and additional reading and solving exercises (approximately 30 hours).
If you need assistance in finding accommodation we may help you. Please contact Rikke Uhrenholt (rwu@cs.aau.dk)
Monday 13.00-14.00 Automatic Verification (chapter 6 in Software Reliability Methods)
Monday 14.00-15.30 SPIN I (provided by Ulrik Nyman)
Tuesday 10.00-11.00 Translating from Logic to Automata (chapter 6 in Software Reliability Methods)
Tuesday 11.00-12.00 The SPIN System
Tuesday 12.00-13.00 Lunch
Tuesday 13.00-14.00 Fairness, Abstractions
Tuesday 14.00-15.30 SPIN II (provided by Ulrik Nyman)
Exercises (solutions to be emailed to Kim — kgl@cs.aau.dk) — by Tuesday February 22, 2011)
Exercise 5.1, 5.2, 5.4, 5.6 and 5.14 (using the constructions(s) provided by Doron) from the following snippet of Joost-Pieter Katoen and Christel Baier: Principles of Model Checking
E. M. Clarke, O. Grumberg, D. A. Peled. Model Checking. MIT Press; 2000.
C. Baier, J-P. Katoen. Principles of Model Checking. MIT Press; 2008.
E. A. Emerson, E. M. Clarke. Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Science of Computer Programming, Vol. 2; pp. 241-266; 1982.
J.Queille, J.Sifakis. Specication and Verication of Concurrent Systems in Caesar. 5th International Symposium on Programming; LNCS 137; Springer; pp. 337-351; 1981.
R. Gerth, D. Peled, M. Vardi, P. Wolper. Atomatic Simple on-the-fly Automatic Verication of Linear Temporal Logic. PSTV’95; pp. 3-18; 1995.
Previously Registered Participants:
Claus Thrane
Danny Poulsen
Jiri Srba
Jonas van Vliet
Kenneth Lausdahl
Kenneth Yrke Jørgensen
Line Juhl
Mads Christian Olesen
Radu Mardare
Rong Pan
Saleem Vighio
Sebastian Bauer
Sune Wolff
MS. Arifa Bhutto
Mikael Harkjær Møller
Yingke Chen
Phan Anh Dung
Simon Laursen
Fabrizio Biondi
Ulrik Mathias Nyman
Thomas Bøgholm
Mikkel Larsen Pedersen
Saulius Samulevicius
Dalia Kaulakiene
Wang Zheng
This entry was posted in news. Bookmark the permalink. Comments are closed, but you can leave a trackback: Trackback URL.
Model Checking PhD course
.. by Doron Peled, Bar Ilan University, Israel, Aalborg University
February 7, 8 2011, Room 0.2.12, Selma Lagerlöfsvej 300, 9220 Aalborg.
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. Amongst several books, together with Ed Clarke and Orna Grumberg, Doron Peled is the (co-) author of the authority book on the subject.
Marktoberdorf 2010, Vicotory
“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.
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:
Time, Venue, ECTS, … :
Schedule:
Exercises (solutions to be emailed to Kim — kgl@cs.aau.dk) — by Tuesday February 22, 2011)
Registration:
References:
Previously Registered Participants: