The VerCors Tool for Verification of Concurrent Programs

Stefan Blom, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

23 Citations (Scopus)
85 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 languageUndefined
Title of host publicationProceedings of the 19th International Symposium on Formal Methods, FM 2014
EditorsCliff Jones, Pekka Pihlajasaari, Jun Sun
Place of PublicationBerlin
PublisherSpringer
Pages127-131
Number of pages5
ISBN (Print)978-3-319-06409-3
DOIs
Publication statusPublished - May 2014
Event19th International Symposium on Formal Methods - Singapore, Singapore
Duration: 12 May 201416 May 2014
Conference number: 19th

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume8442
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference19th International Symposium on Formal Methods
Abbreviated titleFM 2014
CountrySingapore
CitySingapore
Period12/05/1416/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

Cite this

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 (pp. 127-131). (Lecture Notes in Computer Science; Vol. 8442). Berlin: Springer. https://doi.org/10.1007/978-3-319-06410-9_9
Blom, Stefan ; Huisman, Marieke. / The VerCors Tool for Verification of Concurrent Programs. Proceedings of the 19th International Symposium on Formal Methods, FM 2014. editor / Cliff Jones ; Pekka Pihlajasaari ; Jun Sun. Berlin : Springer, 2014. pp. 127-131 (Lecture Notes in Computer Science).
@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",
year = "2014",
month = "5",
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 proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - The VerCors Tool for Verification of Concurrent Programs

AU - Blom, Stefan

AU - Huisman, Marieke

N1 - eemcs-eprint-25487

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

ER -

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