the 9th International Conference on Formal Modeling and Analysis of Timed Systems, will take place at Phønix Hotel, Aalborg, Denmark, from 21 to 23 September 2011.

Invited Talks

• Rajeev Alur, University of Pennsylvania, Philadelphia
  Interfaces for Control Components
• Boudewijn Haverkort, University of Twente, Enschede, and Embedded Systems Institute, Eindhoven
  Formal Modeling and Analysis of Timed Systems: Technology Push or Market Pull?
• Oded Maler, VERIMAG, Grenoble
  Performance Evaluation of Schedulers in a Probabilistic Setting

.. 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.
• Aalborg University, Selma Lagerlöfsvej 300, Room 0.2.90, 9220 Aalborg, Denmark.
• 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)

Schedule:

• Monday 10.00-12.00 Introduction, Specification Formalisms (LTL) (chapter 5 in Software Reliability Methods)
  
• Monday 12.00-13.00 Lunch
• 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
• SPIN exercises

Registration:

• For registration send email to Kim G. Larsen (kgl@cs.aau.dk) before February 3rd, 2011.

References:

1. D. Peled: Model Checking (23 pages) Mandatory Reading.
2. D. Peled: Software Reliability Methods. Springer; 2001 Main Reading  (we will have a 5 copies available that you may borrow).
3. Slides: http://www.dcs.warwick.ac.uk/~doron/big.ppt
4. E. M. Clarke, O. Grumberg, D. A. Peled. Model Checking. MIT Press; 2000.
5. C. Baier, J-P. Katoen. Principles of Model Checking. MIT Press; 2008.
6. 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.
7. J.Queille, J.Sifakis. Specication and Verication of Concurrent Systems in Caesar. 5th International Symposium on Programming; LNCS 137; Springer; pp. 337-351; 1981.
8. 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