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.

Related 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.


Personal tools