Tools and Methods for Scalable Software Verification (TOMESO)

From PLSwiki

Jump to: navigation, search


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.


  • 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)


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.
  • Kopitiam (Eclipse plugin integrating Java development with verification) can be found here.

Stays abroad


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.

Meeting schedule

In the spring 2012, the project meetings are Fridays 10:00-12:00, in room 4A09.

Personal tools