Daniel Hirschkoff

Separation logic is an extension of Floyd-Hoare logic that makes it possible to reason about programs manipulating pointers. Since its introduction at the beginning of this millenary, it has led to several developments, which include tools for the automatic verification of properties of pointer manipulating programs, as well as reasoning about concurrent programs in a shared memory scenario.

This research school will take place in the week Jan.31st-Feb. 4, 2011.

Courses will be taught in english.

Slides:

HYang, intro, sep-logic, hiding, automation

AGotsman, concurrency, csl, lockfree, scheduler

MParkinson,abstract predicates, rely-guarantee, RGSep, deny-guarantee

Code: reverse.c, create.c, dispose.c, push.c, pop.c

The lecture notes on Separation Logic, written by J. Reynolds and mentioned by H. Yang in his lecture, are available here.

The prerequisite to follow the course is a basic knowledge of first-order logic.

Tool exercises: we suggest that attendees bring a laptop for the sessions devoted to tool exercises. Exercises will be made using the Verifast Program Verifier (follow the link to download and install the tool on your computer).

Lecturers

  • Hongseok Yang (Lecturer, Queen Mary University of London, UK)
  • Alexey Gotsman (Assistant Professor, IMDEA, Spain)
  • Matthew Parkinson (Researcher, Microsoft Research, Cambridge, UK)

Topics (tentative description)

1) Basic separation logic.

  • [a] Basic proof rules and semantics of separation logic.
  • [b] Basic automatic verification algorithms based on separation logic.

2) Logic-based approaches on information hiding and data abstraction.

  • [a] Higher-order frame rules and abstract predicates.
  • [b] Automatic verification algorithm with abstract predicates.

3) Invariant-based approaches on the verification of concurrent programs.

  • [a] Concurrent separation logic.
  • [b] Automatic verification algorithm based on concurrent separation logic.

4) Rely-Guarantee.

  • [a] RGSep: the marriage of rely-guarantee and separation logic.
  • [b] Automatic verification with RGSep.
  • [c] Reasoning about liveness properties.
  • [d] Deny Guarantee.

Tentative schedule for the week. [L] means a lecture, and [E] means an exercise session.

Mon (5 hours)

  • [L] Introduction and basic semantics (HY)     10h30
  • [E] Introduction and basic semantics (HY)
  • [E] Concurrent programming (AG)      14h00
  • [L] Basic separation logic (HY)
  • [E] Basic separation logic (HY)

Tue (5 hours)

  • [L] Abstract predicate (MP)     9h00
  • [E] Abstract predicate (MP)
  • [E] Tool exercise 1 (AG)
  • [L] Information hiding (HY)   14h00
  • [E] Information hiding (HY)

Wed (7 hours)

  • [L] Concurrent separation logic (AG)     9h00
  • [E] Concurrent separation logic (AG)
  • [E] Tool exercise 2 (AG)
  • [L] RGSep (MP)              13h30
  • [E] RGSep (MP)
  • [L] Automation (HY)     16h00
  • [E] Automation (HY)

Thu (4 hours)

  • [L] Soundness of concurrent separation logic (AG)        9h00
  • [L] Deny/Guarantee (MP)
  • [E] Deny/Guarantee (MP)
  • [L] ..

Fri (3+1 hours)

  • [L] Liveness (AG)          9h00
  • [E] Liveness (AG)
  • [L] Concurrent abstract predicate (MP)
  • Exam     (end: 13h00)

Please contact Daniel Hirschkoff if you have any question regarding this course.