The VerCors Tool for Verification of Concurrent Programs

Stefan Blom; Marieke Huisman

doi:10.1007/978-3-319-06410-9_9

The VerCors Tool for Verification of Concurrent Programs

Stefan Blom, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

34 Citations (Scopus)

305 Downloads (Pure)

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.

Original language	Undefined
Title of host publication	Proceedings of the 19th International Symposium on Formal Methods, FM 2014
Editors	Cliff Jones, Pekka Pihlajasaari, Jun Sun
Place of Publication	Berlin
Publisher	Springer
Pages	127-131
Number of pages	5
ISBN (Print)	978-3-319-06409-3
DOIs	https://doi.org/10.1007/978-3-319-06410-9_9
Publication status	Published - May 2014
Event	19th International Symposium on Formal Methods - Singapore, Singapore Duration: 12 May 2014 → 16 May 2014 Conference number: 19th

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	8442
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	19th International Symposium on Formal Methods
Abbreviated title	FM 2014
Country/Territory	Singapore
City	Singapore
Period	12/05/14 → 16/05/14

Keywords

EC Grant Agreement nr.: FP7/2007-2013
EC Grant Agreement nr.: FP7/258405
EC Grant Agreement nr.: FP7/287767
METIS-309765
Separation Logic
Verification Tools
IR-94062
EWI-25487

Access to Document

10.1007/978-3-319-06410-9_9

http://eprints.eemcs.utwente.nl/secure2/25487/01/fm2014-tool-official.pdf

Cite this

@inproceedings{789e571068504757998a0a028fb6b9f1,

title = "The VerCors Tool for Verification of Concurrent Programs",

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.",

keywords = "EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/258405, EC Grant Agreement nr.: FP7/287767, METIS-309765, Separation Logic, Verification Tools, IR-94062, EWI-25487",

author = "Stefan Blom and Marieke Huisman",

note = "eemcs-eprint-25487 ; null ; Conference date: 12-05-2014 Through 16-05-2014",

year = "2014",

month = may,

doi = "10.1007/978-3-319-06410-9_9",

language = "Undefined",

isbn = "978-3-319-06409-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "127--131",

editor = "Cliff Jones and Pekka Pihlajasaari and Jun Sun",

booktitle = "Proceedings of the 19th International Symposium on Formal Methods, FM 2014",

}

Blom, S & Huisman, M 2014, The VerCors Tool for Verification of Concurrent Programs. in C Jones, P Pihlajasaari & J Sun (eds), Proceedings of the 19th International Symposium on Formal Methods, FM 2014. Lecture Notes in Computer Science, vol. 8442, Springer, Berlin, pp. 127-131, 19th International Symposium on Formal Methods, Singapore, Singapore, 12/05/14. https://doi.org/10.1007/978-3-319-06410-9_9

The VerCors Tool for Verification of Concurrent Programs. / Blom, Stefan; Huisman, Marieke.

Proceedings of the 19th International Symposium on Formal Methods, FM 2014. ed. / Cliff Jones; Pekka Pihlajasaari; Jun Sun. Berlin : Springer, 2014. p. 127-131 (Lecture Notes in Computer Science; Vol. 8442).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - The VerCors Tool for Verification of Concurrent Programs

AU - Blom, Stefan

AU - Huisman, Marieke

N1 - Conference code: 19th

PY - 2014/5

Y1 - 2014/5

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

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

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - EC Grant Agreement nr.: FP7/258405

KW - EC Grant Agreement nr.: FP7/287767

KW - METIS-309765

KW - Separation Logic

KW - Verification Tools

KW - IR-94062

KW - EWI-25487

U2 - 10.1007/978-3-319-06410-9_9

DO - 10.1007/978-3-319-06410-9_9

M3 - Conference contribution

SN - 978-3-319-06409-3

T3 - Lecture Notes in Computer Science

SP - 127

EP - 131

BT - Proceedings of the 19th International Symposium on Formal Methods, FM 2014

A2 - Jones, Cliff

A2 - Pihlajasaari, Pekka

A2 - Sun, Jun

PB - Springer

CY - Berlin

Y2 - 12 May 2014 through 16 May 2014

ER -