Tools and Methods for Scalable Software Verification (TOMESO)
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.
- Filip Sieczkowski (PhD student, defense expected February 2014)
- Hannes Mehnert (PhD student, dissertation hand in June 2013, defense 11 October 2013)
- Jakob Thamsborg (post doc)
- Jesper Bengtson (post doc)
- Kasper Svendsen (post doc)
- Jonas Buhrkal Jensen (PhD student, dissertation hand in September 2013, defense 17 December 2013)
- Lars Birkedal (principal investigator)
- Peter Sestoft (principal investigator)
- K. Svendsen, L. Birkedal and M. Parkinson. Modular Reasoning about Separation of Concurrent Data Structures. ESOP 2013.
- J. Jensen, N. Benton and A. Kennedy. High-level Separation Logic for Low-Level Code. POPL 2013.
- J. Schwinghammer, L. Birkedal, F. Pottier, B. Reus, K. Støvring, and H. Yang. A step-indexed Kripke model of hidden state. To Appear in Mathematical Structures in Computer Science, 2012.
- J. Bengtson, J. Jensen, and L. Birkedal. Charge! -- A framework for higher-order separation logic in Coq. ITP 2012.
- J. Mackay, H. Mehnert, A. Potanin, L. Groves and N. Cameron Encoding Featherweight Java with Assignment and Immutability using The Coq Proof Assistant. FTfJP 2012
- H. Mehnert and J. Aldrich Verification of Snapshotable Trees using Access Permissions and Typestate. TOOLS 2012
- J. Jensen and L. Birkedal. Fictional Separation Logic. ESOP 2012.
- H. Mehnert, F. Sieczkowski, L. Birkedal, and P. Sestoft. Formalized verification of snapshotable trees: Separation and sharing. VSTTE 2012
- L. Birkedal, F. Sieczkowski, and J. Thamsborg. A concurrent logical relation. CSL 2012.
- L. Birkedal, K. Støvring, and J. Thamsborg. A relational realizability model for higher-order stateful ADTs. Journal of Logic and Algebraic Programming 2012.
- J. Schwinghammer, L. Birkedal, B. Reus, and H. Yang. Nested Hoare triples and frame rules for higher-order store. Logical Methods in Computer Science, 7(3:21), July 2011.
- J. Bengtson, J. Jensen, F. Sieczkowski, and L. Birkedal. Verifying object-oriented programs with higher-order separation logic in Coq. ITP 2011.
- H. Mehnert Kopitiam: modular incremental interactive full functional static verification of Java code. NFM 2011.
- J. Thamsborg and L. Birkedal. A Kripke logical relation for effect-based program transformations. ICFP 2011.
- K. Svendsen, L. Birkedal, and A. Nanevski. Partiality, state, and dependent types. TLCA 2011.
- A. Buisse, L. Birkedal, and K. Støvring. A step-indexed kripke model of separation logic for storable locks. MFPS 2011
- J. Jensen, L. Birkedal, and P. Sestoft. Modular Verification of Linked Lists with Views via Separation Logic. Journal of Object Technology, 2011.
- L. Birkedal, B. Reus, J. Schwinghammer, K. Støvring, J. Thamsborg, and H. Yang. Step-indexed kripke models over recursive worlds. POPL 2011.
- K. Svendsen, L. Birkedal, and M. Parkinson. Verifying Delegates and Generics. ECOOP 2010.
- J. Jensen. Specification and Validation of Data Structures using Separation Logic. M.Sc. dissertation. March 2010.
- L. Birkedal, K. Støvring, and J. Thamsborg. The category-theoretic solution of recursive metric-space quations. Theoretical Computer Science 2010.
- L. Birkedal, K. Støvring, and J. Thamsborg. Realizability semantics of parametric polymorphism, general references, and recursive types. Mathematical Structures in Computer Science 2010.
Other related publications can be found here.
- Current version of formalization of Separation Logic in Coq for Object-Oriented languages can be found here.
- Kopitiam (Eclipse plugin integrating Java development with verification) can be found here.
- Filip Sieczkowski visited Viktor Vafeiadis at Max Planck Institute for Software Systems from June 2012 to September 2012.
- Jonas Jensen visited Nick Benton at Microsoft Research Cambridge from March 2012 to May 2012.
- Hannes Mehnert visited Jonathan Aldrich at Carnegie Mellon University from September 2011 to March 2012.
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.
In the spring 2012, the project meetings are Fridays 10:00-12:00, in room 4A09.