Back to University of Twente portal
| author: | Martijn Roo |
| title: | Specifying Concurrent Programs: a Case Study in JML and Separation Logic |
| keywords: | |
| topics: | Algorithms and Data Structures , Case studies and Applications |
| committee: |
Marieke Huisman
, Marina Zaharieva-Stojanovski |
| end: | 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