Capita Selecta Software Engineering 2011-2012 (Leuven): Verification of Imperative Programs

Instructor: Bart Jacobs; co-instructor: Jan Smans

Exam

• For K.U.Leuven students: Homework assignment + oral defense.
• For non-K.U.Leuven students: Homework assignment.

NEW: Assignment. Deadline for handing in the assignment: Friday, April 27 2012, 16:00. Note: upgrade to VeriFast 11.11.27 before starting the assignment.

Note: All students have to participate in all three modules (Leuven, Brussels, Antwerp) of the course. Not participating in any module automatically leads to a failing grade for the entire course.

Classes

Three PC-lab sessions of 4 hours each, where students perform the exercises from the VeriFast tutorial. (A hardcopy of the tutorial will be provided.)

• Class 1: Monday, 3 October 2011, 15:00-19:00, room VHI 01.25 (LUDIT PC-KLAS G1) (Note: at 17:00, we move to VHI 02.24 (LUDIT PC-KLAS F2))
• Class 2: Monday, 10 October 2011, 15:00-19:00, room VHI 02.23 (LUDIT PC-KLAS E2) (Note: at 17:00, we move to VHI 02.24 (LUDIT PC-KLAS F2))
• Class 3: Monday, 17 October 2011, 15:00-19:00, room MTC1 02.15 (PC-lokaal)

Building VHI = Van Den Heuvelinstituut, Dekenstraat 2, 3000 Leuven (a 10-minute walk from the train station)
Building MTC1 = Maria-Theresiacollege, Sint-Michielsstraat 6, 3000 Leuven (a 15-minute walk from the train station)

Course Content

The students will be taught the VeriFast approach for verifying various correctness properties of single-threaded and multithreaded imperative programs. The language used will be C but the approach is equally applicable to C++, Java, C#, etc. Supported correctness properties include absence of data races, absence of buffer overflows, absence of memory leaks, and programmer-specified preconditions and postconditions. Properties are specified using separation logic and verified using symbolic execution.

Contrary to most other verification approaches, like model checking, the approach taught in this class is modular, so that it scales linearly with the size of the program; and it supports infinite state spaces and arbitrarily complex properties.

Background literature

• On VeriFast: See the VeriFast website
• On data races
  • Hans Boehm. Threads Basics. An introduction to data races and why they are bad.
  • H. Boehm and S. Adve. Foundations of the C++ concurrency model. PLDI 2008.
  • Threads and Locks, Chapter 17 of The Java Language Specification, Third Edition (Note: Sections 17.4.8, 17.4.9, and 17.5 are not relevant to this course.) The official specification of how memory behaves in a multithreaded Java program.
  • Correctly Synchronized Programs. Section 2.1 in: J. Manson, W. Pugh, and S. Adve. The Java Memory Model. POPL 2005.
• On separation logic
  • J. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. LICS 2002.
  • A. Gotsman, J. Berdine, B. Cook, N. Rinetzky, and M. Sagiv. Local Reasoning for Storable Locks and Threads. APLAS 2007.

See also

• Capita Selecta Software Engineering 2011-2012 (Brussels) (instructor: Dr. Bruno De Fraine)
• Capita Selecta Software Engineering 2011-2012 (Antwerp) (instructor: Prof. Serge Demeyer)