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 Bengtsson (post doc)
- Jonas Braband Jensen (PhD student)
- Lars Birkedal (principal investigator)
- Peter Sestoft (principal investigator)
Publications
- 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.
Related Work
- B. Jacobs, J, Smans, and F. Piessens VeriFast: Imperative Programs as Proofs (website with tool and further work)
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
Seminar schedule
In the Fall 2010, the project meetings are Fridays 10-12, in room 4A 09.
There is an associated Ph.D. course on Modular Software Verification.
