T-79.5305 Formal Methods (4 cr) P V

Autumn 2006

The course T-79.5305 replaces the course T-79.157 Formal Description and Verification of Computing Systems.

Model checking is a technique to algorithmically verify hardware and software systems. It has been succesfully applied to analyze hardware systems and is currently a part of the development process in many hardware design companies such as Intel and IBM. Compared to hardware systems, model checking software systems poses new challenges due to a larger number and domains of variables involved, dynamic memory allocation, more complex concurrency primitives, and in general larger system sizes. These problems have been tackled in the research literature during the last few years, enabling the analysis of more and more complex software systems.

One of the main techniques applied in software model checking is abstraction. The goal of abstraction is to remove parts of the system that are irrelevant to the verification of the desired property either in an exact or over-approximating way. If over-approximation is used, then the analysis may report false negatives (i.e. bugs that are not real bugs in the system) and the applied abstraction has to be refined in order to remove the false negative. As an example of industrial use of abstraction techniques in software system verification, the Static Driver Verifier tool, developed in the SLAM project at Microsoft, relies on so-called predicate abstraction. The tool has recently been beta-released as part of the Windows Driver Foundation. Other similar projects include e.g. Bandera that develops a tool set for model checking concurrent Java software, and Blast providing a software model checker for C programs.

In this course, we will go through research material concerning different abstraction techniques and other similar techniques. The course is organized in a seminar form.

Current

• [25 Aug 2006] First lecture Wednesday 13th of September, room TB353.

General

• Coordinator: Dr. Tommi Junttila
• Tutors: Prof. Ilkka Niemelä, Doc. Keijo Heljanko, and Lic.Sc.(Tech.) Heikki Tauriainen
• Seminar meetings: On Wednesdays from 16.15 onwards in the seminar room TB353. The first meeting will be on Wednesday 13th of September.
• Prerequisites: Basic knowledge of problem representations and logic (T-79.1001, T-79.3001); parallel and distributed systems (T-79.4301); basic knowledge on programming languages (Java, C, etc.)
• Requirements for passing the course:
  • Attend the seminars (recommended, not required).
  • Give a seminar presentation. The length of the presentation should be 45-90 minutes.
  • Write a short report (5-8 pages) on your presentation topic. The report shoud review the problem, solution, and techniques in the presentation material and include a small self-made example on applying the solution/techniques. The deadline for delivering the report is the wednesday two weeks after your presentation.
  • Act as an opponent for one other presentation. This includes reading the presentation material, preparing and presenting two questions, and generally being active during the presentation.
• Course web site: http://www.tcs.hut.fi/Studies/T-79.5305/

Schedule (tentative)

• Wednesday September 13th. First meeting, introductory slides

• Wednesday September 20th. Presentation by Dubrovin, tutor Junttila, opponent Korpela:

  Clarke et al. Model Checking and Abstraction. ACM Transactions on Programming Languages and Systems 16(5), pages 1512-1542, 1994.

  For an overview of the material of this and the following presentation, see also "Progress on the State Explosion Problem in Model Checking" by Clarke et al.

• Wednesday September 27th. Presentation by Ojala, tutor Junttila, opponent Dubrovin:

  Clarke et al. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM 50(5), pages 752-794, 2003.

  For an overview, see also the conference version "Counterexample-guided abstraction refinement" by Clarke et al.

• Wednesday October 4th. Presentation by Kylmälä, tutor Junttila, opponent Pitkämäki:

  Visser et al. Model Checking Programs, not sections 3.3.2 and 3.3.3.

  Lerda and Visser. Addressing Dynamic Issues of Program Model Checking.

• Wednesday October 11th. Presentation by Pitkämäki, tutor Tauriainen, opponent Pietiläinen:

  Hatcliff et al. Foundations of the Bandera Abstraction Tools.

  Pasareanu et al. Finding feasible abstract counter-examples.

  For an overview of Bandera, see also: Corbett et al. Bandera: extracting finite-state models from Java source code.

• Wednesday October 18th. Presentation by Lampinen, tutor Heljanko, opponent Kähkönen:

  Ball et al. Thorough Static Analysis of Device Drivers.

  Ball et al. Automatic Predicate Abstraction of C Programs.

  Ball and Rajamani. Automatically Validating Temporal Safety Properties of Interfaces.

• Wednesday October 25th. Presentation by Korpela, tutor Heljanko, opponent Kettunen:

  Esparza et al. Efficient Algorithms for Model Checking Pushdown Systems.

  Esparza and Schwoon. A BDD-based Model Checker for Recursive Programs.

  Suwimonteerabuth et al. jMoped: A Java Bytecode Checker Based on Moped.

• Wednesday November 1st.

  Examination week, no presentation unless really necessary.

• Wednesday November 8th. Presentation by Hyvärinen, tutor Niemelä, opponent Ojala:

  Chaki et al. Efficient Verification of Sequential and Concurrent C Programs.

• Wednesday November 15th. Presentation by Kähkönen, tutor Niemelä, opponent Hyvärinen:

  Henzinger et al. Lazy Abstraction.

• Wednesday November 22nd. Presentation by Pietiläinen, tutor Niemelä, opponent Kylmälä:

  Clarke et al. Predicate Abstraction of Ansi-C Programs Using SAT.

  Kroening and Clarke. Checking Consistency of C and Verilog using Predicate Abstraction and Induction.

• Wednesday November 29th. Presentation CANCELED!

  Presentation by Kettunen, tutor Tauriainen, opponent Lampinen:

  Hatcliff et al. A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives

  Ranganath et al. A New Foundation for Control-Dependence and Slicing for Modern Program Structures

  For a longer report version, see also Ranganath et al. A New Foundation for Control-Dependence and Slicing for Modern Program Structures

  For a tutorial on slicing, see e.g. this

• Wednesday December 13th.

  No presentation.

Background material

• The lecture slides of Parallel and distributed systems
• Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. The MIT Press, 1999. Especially the following chapters:
  • Chapters 2, 3, and 4: modelling, temporal logics, and model checking.
  • Chapters 5 and 6: Binary decision diagrams and symbolic model checking.
  • Chapter 9: Model checking and automata theory.
  • Chapter 10: Partial order methods.