NB: The information concerns the course given in 1998

News and Links

• Verus (a Real Time LTL model checker from CMU) is now installed at IDA. Verus can be run by typing e.g. /home/logpro/bin/verus /home/logpro/systems/verus/examples/mutex2.ver. There is a postscript manual in /home/logpro/systems/verus/vmanual.ps.

• Spin (a LTL model checker from Bell Labs) and Xspin are now installed at IDA. Xspin can be run by typing /home/logpro/bin/xspin. Information about Spin can be found here.

• Some stuff on BDDs, by Bryant. Some more stuff by Dill.

• Tentative list of participants

• The SMV system has been installed on IDA's research domain. To run the system, write module add /home/logpro/modules/logpro and then use the command smv ARGUMENTS. A postscript manual is available from CMU. Some examples can be found in /home/logpro/systems/smv/examples. NOTE: If you are not sitting on ida.liu.se you have to download the system yourself.

• Report on strategic directions in Computing Research: The Formal Methods working group.

• Virtual library: Formal Methods

• Virtual library: Safety-Critical Systems

Prerequisites

Basic knowledge in logic, discrete mathematics and automata theory.

Organization

Seminars with presentations by participants.

Content

Tentative schedule:

Fri 20/3 10-12 Eliten    Planning meeting

Wed 25/3 15-17 Belön     General Introduction
                         Wlodek Drabent

Wed  1/4 15-17 Belön     Modeling and temporal logics (Ch 3 + 4)
                         Radek Szymanek/Kris Kuchcinski

Wed  8/4 15-17 Estrad    Model checking (Ch 5)
                         Johan Lübcke/Jan Maluszynski
                         
Wed 22/4 15-17 Belön     Symbolic methods (Ch 6, 7.1, 7.2)
                         Dan Lawesson/Jacek Malec

Wed 29/4 15-17 Galleriet Symbolic methods (contd) (Ch 7.3-7.8)          
                         Patrik Haslum

Wed  6/5 15-17 Belön     Model checking and automata theory (Ch 8)
                         Peter Loborg

Wed 13/5 15-17 Belön     Equivalence, ordering and composition (Ch 10+11)
                         Marcus Bjäreland/Simin Nadjm-Tehrani

Fri 15/5 10-12 Eliten    Abstraction (Ch 12)
                         Ulf Nilsson/Per Andersson

Wed 27/5 15-17 Belön     Discrete real-time systems (Ch 16)
                         Jacek Malec/Man Lin

Tue  9/6 13-15 Gryningen Model checking for the mu-calculus (Ch 17)
                         Lars Lindqvist

Literature

Clarke, Grumberg and Peled, Model Checking, book draft, 1998.

Examination and credits

Active participation, presentations and errata give 3+ credits.