Tools and Methods for Scalable Software Verification (TOMESO)
From PLSwiki
Contents |
Project goals
The goals of the project are: (1) To apply theoretical advances in program logics, and in particular separation logic, to practice, (2) to develop prototype software tools for formal specification with separation logic, (3) to apply the prototypes in a case study, and (4) to give methodological advice on to structure software so as to facilitate formal specification and proof about it, and give advice on how to conduct such proofs.
By identifying and addressing the research questions that arise in the process, we hope to ultimately increase our ability to produce correct software. As the central case we consider the C5 collection class library.
People
- Filip Sieczkowski (PhD student)
- Hannes Mehnert (PhD student)
- Jakob Thamsborg (post doc)
- Jesper Bengtson (post doc)
- Jonas Braband Jensen (PhD student)
- Lars Birkedal (principal investigator)
- Peter Sestoft (principal investigator)
Publications
- J. Bengtson, J.B. Jensen, F. Sieczkowski, and L. Birkedal. Verifying object-oriented programs with higher-order separation logic in Coq Accepted for publication at ITP 2011.
- H. Mehnert Kopitiam: modular incremental interactive full functional static verification of Java code Accepted for publication at NFM 2011.
- K. Svendsen, L. Birkedal, and M. Parkinson. Verifying Delegates and Generics. Accepted for publication in ECOOP 2010.
- J. Jensen. Specification and Validation of Data Structures using Separation Logic. M.Sc. dissertation. March 2010.
Other related publications can be found here.
Source Code
- Current version of formalization of Separation Logic in Coq for Object-Oriented languages can be found here.
Funding
The project is funded by a grant from the Danish Council for Independent Research | Technology and Production Sciences (FTP), and by the IT University of Copenhagen, in the period 2009-2013.
Seminar tracks
- (1) Coq implementation (syntax and semantics) for a subset of Java
- (2) Identify further C5 challenge verifications
- (3) Survey (semi-)automatic tools
- (4) Related logic approaches
- (5) Relations to concurrency
Meeting schedule
In the spring 2011, the project meetings are Fridays 12:30-14:30, in room 4A09.
| Date | Speaker | Comments |
|---|---|---|
| Jan 7 | cancelled | |
| Jan 14 | Jacob | |
| Jan 21 | Jonas | |
| Jan 28 | cancelled (Lars away, Peter away) | |
| Feb 4 | ||
| Feb 11 | Lars | |
| Feb 18 | Hannes | Lars away. Hannes talks about snapshottable trees |
| Feb 25 | Peter | Peter talks about the composite pattern |
| Mar 4 | Jesper | |
| Mar 11 | Hannes | Kopitiam: current state (including live demonstration and future development) |
| Mar 18 | Jesper+Lars+Hannes away | |
| Mar 25 | Jesper+Jonas away | |
| Apr 1 | Jesper+Lars away | |
| Apr 8 | Joe | Reasoning about Concurrency in (RT) Java Media:Kiniry-TOMESO.pdf |
| Apr 15 | Jonas,Hannes | Hannes NASA practice talk (15 min) + Jonas talks about sharing |
| Apr 22 | cancelled (Easter) | |
| Apr 29 | cancelled (Anders Schack-Nielsen's PhD defence) | |
| May 6 | Filip | Filip talks about sharing |
| May 13 | Kasper | How to Make Ad Hoc Proof Automation Less Ad Hoc |
| May 20 | cancelled (silly religious holiday) | |
| May 27 | Jesper | (Practical) Tactics for Separation Logic. (Jonas away) |
| Jun 3 | day after Ascension day (Jonas, Hannes away) | |
| Jun 10 | Split in two meetings: Coq hacking and snap-trees | |
| Jun 17 | (Jonas, Jesper, Filip away) | |
| Jun 24 | (Jesper, Filip away) | |
| Jul 1 | (Jonas, Jesper, Filip, Peter away) | |
| Jul 8 | (Jonas, Peter away) | |
| ? | Lars | New SL for concurrency |
