Tools and Methods for Scalable Software Verification (TOMESO)

From PLSwiki

Jump to: navigation, search

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

Publications

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
Personal tools