The VerCors tool for verification of concurrent programs
The work
| Authors | Stefan Blom; Marieke Huisman |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2014 |
| Citekey | blom2014vercors |
Where it appeared
| Published in | International Symposium on Formal Methods |
|---|---|
| Publisher | Springer |
| Series | Lecture Notes in Computer Science |
| Number in series | 8442 |
| Pages | 127--131 |
Identifiers
| DOI | 10.1007/978-3-319-06410-9_9 |
|---|
Related
| Distinct from | blom2017vercors |
|---|
Abstract
The VerCors tool implements thread-modular static verification of concurrent programs, annotated with functional properties and heap access permissions. The tool supports both generic multithreaded and vector-based programming models. In particular, it can verify multithreaded programs written in Java, specified with JML extended with separation logic. It can also verify parallelizable programs written in a toy language that supports the characteristic features of OpenCL. The tool verifies programs by first encoding the specified program into a much simpler programming language and then applying the Chalice verifier to the simplified program. In this paper we discuss both the implementation of the tool and the features of its specification language.
A copy is held
pdf, 136.9 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-28 21:27 UTC |
Filed under
Cite it as
@inproceedings{blom2014vercors,
title = {The VerCors tool for verification of concurrent programs},
author = {Stefan Blom and Marieke Huisman},
year = {2014},
booktitle = {International Symposium on Formal Methods},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
pages = {127--131},
doi = {10.1007/978-3-319-06410-9_9},
}
This record lives at https://refs.drheap.org/blom2014vercors/ and will keep doing so.