From PLSwiki

Jump to: navigation, search


Modular Software Verification Ph.D. Course, Fall 2010

We'll read and discuss a bunch of papers. There will be some means of obtaining ECTS.

Organizer: Lars Birkedal.

Credit: 7.5 ECTS

Evaluation: Ph.D. students can get credit by active participation and by giving one-two presentations of research papers.

When and where: Tuesdays 13:30-15:30, room 2A05. Except September 28th in room 3A07.


Homepage up and running!

Oct. 13th.: Fall Break in week 42. Everything is pushed one week forward. Alex loses one slot.

Nov. 15th.: Jesper's presentation gets one more slot. Everything is pushed one week forward. Fabrizio loses one slot.

Nov. 15th.: Peter and Jonas exchanged slots.

Dec. 6th.: John Reynolds grabbed Alex's slot. Subject to be announced.

Topics and tentative plan

Week Date Presenter Topic Paper(s)
36 Tue 07 Sep Thamsborg Region Logic [1]
37 Tue 14 Sep Thamsborg Applied Region Logic: The Composite Pattern [2]
38 Tue 21 Sep Filip Type states / API protocol compliance [3], [4]
39 Tue 28 Sep Jan Schwinghammer Capability Calculus Main focus is step-indexed model from Section 3 of [5]. See also

[6] for a more thorough introduction to step-indexing.

40 Tue 05 Oct Hannes Compositional Shape by means of Bi-Abduction [7]
41 Tue 12 Oct Hannes Compositional Shape by means of Bi-Abduction [8]
42 Tue 19 Oct N/A Fall Break [9]
43 Tue 26 Oct Jonas Interfaces in OO separation logic Stephan van Staden and Cristiano Calcagno. Reasoning about Multiple Related Abstractions with MultiStar. [10]
44 Tue 02 Nov Filip Resources, Concurrency and Local Reasoning PW O'Hearn, Theoretical Computer Science 375(1-3) , pp271-307, May 2007.
45 Tue 09 Nov Jesper RG-Sep, A marriage of rely/guarantee and separation logic Viktor Vafeiadis, Matthew Parkinson. CONCUR 2007. LNCS, vol. 4703, pp. 256-271. Springer (Sep. 2007), Chapters 1 - 4 of Viktor Vafeiadis' dissertation, [11] (references)
46 Tue 16 Nov Jesper RG-Sep continued.
47 Tue 23 Nov Peter Sestoft Abstraction and Refinement for Local Reasoning Dinsdale-Young, Gardner, Wheelhouse, VSTTE 2010
48 Tue 30 Nov Jonas Local Rely-Guarentee Reasoning Local Rely-Guarentee Reasoning, POPL 09 Xinuy Feng [12]
49 Tue 07 Dec Martin Zuziak Concurrent abstract predicates Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew Parkinson, Viktor Vafeiadis. In ECOOP 2010
50 Tue 14 Dec John Reynolds TBA TBA
51 Tue 21 Dec Fabrizio A Separation Logic for the Pi-calculus [13]

Unscheduled topics

Andrew Tolmach mentioned to me at the summer school to look into "Practical Tactics for Separation Logic" by Andrew McCreight [14] publicated at TPHOL 2009.

- Semantics for HTT, Kapser

- Relational Semantics for Effect-based Program Transformations papers by Benton, Beringer, Hofmann, Kennedy, LB / Jacob

- Nested Hoare Triples, LB

Personal tools