PROGRAM VERIFICATION USING SEPARATION LOGIC

Audience

This is a small advanced course addressing PhD students as well as research-oriented Master students. Succesful participation is worth 2 CP ETCS.

Slides from Lectures (including homework exercises)

Lecture 1
Lecture 2
Lecture 3
Lecture 4
Lecture 5

Objectives

The incorrect use of pointers, such as null pointer dereference and memory leaks, is one of the most common (and expensive) sources of program errors.

 

Formal verification of programs using pointers is known to be a very hard task. In this course, we will survey Separation Logic, a recent extension of Hoare logic that addresses the problem of effective reasoning about pointers and allowing therefore efficient verification for this class of programs. Topics of the course will include frame inference, bi-abduction, abstraction, concurrency, and principles of automatic verification based on separation logic.

 


Dates

The course spans the period 21 - 25 September, 2009.

 

Lectures are held daily 09.15 - 11:00 in Hall H3, E1 3.

 

If you want to obtain credit points for this course, please register at the CMS.


Instructor

Dr. Dino Distefano, Queen Mary, University of London