Tomeso-Fall-2010
From PLSwiki
Contents |
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.
News
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
