Martijn Roo - Specifying Concurrent Programs: a Case Study in JML and Separation Logic

author:Martijn Roo
title:Specifying Concurrent Programs: a Case Study in JML and Separation Logic
keywords:
topics:Case studies and Applications, Algorithms and Data Structures
committee:prof.dr. M. Huisman
M. Zaharieva-Stojanovski MSc
graduation date:January 2014


Abstract

This paper presents a case study for the verification of concurrent programs. A model for a central printer server was designed, implemented and annotated with a formal specification in JML, extended with syntax for permission-based separation logic. The specification is compatible with the VerCors toolset which is currently being developed at the University of Twente. The goal of this research has been to design and implement a shared data structure with a formal specification that can be used to test future concurrent program verifiers. The correctness of the program is discussed in natural language and an outline for a formal proof is given.

For the paper see:

http://referaat.cs.utwente.nl/conference/20/paper/7412/specifying-concurrent-programs-a-case-study-in-jml-and-separation-logic.pdf

Additional Resources