Verification of concurrent systems with VerCors

A. Amighi, Stefan Blom, Saeed Darabi, Marieke Huisman, Wojciech Mostowski, M. Zaharieva

  • 5 Citations

Abstract

This paper presents the VerCors approach to verification of concurrent software. It first discusses why verification of concurrent software is important, but also challenging. Then it shows how within the VerCors project we use permission-based separation logic to reason about multithreaded Java programs. We discuss in particular how we use the logic to use different implementations of synchronisers in verification, and how we reason about class invariance properties in a concurrent setting. Further, we also show how the approach is suited to reason about programs using a different concurrency paradigm, namely kernel programs using the Single Instruction Multiple Data paradigm. Concretely, we illustrate how permission-based separation logic is suitable to verify functional correctness properties of OpenCL kernels. All verification techniques discussed in this paper are supported by the VerCors tool set.
Original languageUndefined
Title of host publicationFormal Methods for Executable Software Models - 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems
EditorsMarco Bernardo, Ferruccio Damiani, Reiner Hahnle, Einar Johnsen, Ina Schaefer
Place of PublicationBerlin
PublisherSpringer Verlag
Pages172-216
Number of pages45
ISBN (Print)978-3-319-07316-3
DOIs
StatePublished - Jun 2014

Publication series

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

Fingerprint

Invariance

Keywords

  • EWI-24905
  • CR-D.2.4
  • Software Verification
  • EC Grant Agreement nr.: FP7/2007-2013
  • METIS-305942
  • EC Grant Agreement nr.: FP7/287767
  • VerCors tool
  • IR-91766
  • Concurrency
  • EC Grant Agreement nr.: FP7/258405

Cite this

Amighi, A., Blom, S., Darabi, S., Huisman, M., Mostowski, W., & Zaharieva, M. (2014). Verification of concurrent systems with VerCors. In M. Bernardo, F. Damiani, R. Hahnle, E. Johnsen, & I. Schaefer (Eds.), Formal Methods for Executable Software Models - 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (pp. 172-216). (Lecture Notes in Computer Science; Vol. 8483, No. 8483). Berlin: Springer Verlag. DOI: 10.1007/978-3-319-07317-0_5

Amighi, A.; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva, M. / Verification of concurrent systems with VerCors.

Formal Methods for Executable Software Models - 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems. ed. / Marco Bernardo; Ferruccio Damiani; Reiner Hahnle; Einar Johnsen; Ina Schaefer. Berlin : Springer Verlag, 2014. p. 172-216 (Lecture Notes in Computer Science; Vol. 8483, No. 8483).

Research output: ScientificChapter

@inbook{c5a665234a01466d938d0a17c0995b03,
title = "Verification of concurrent systems with VerCors",
abstract = "This paper presents the VerCors approach to verification of concurrent software. It first discusses why verification of concurrent software is important, but also challenging. Then it shows how within the VerCors project we use permission-based separation logic to reason about multithreaded Java programs. We discuss in particular how we use the logic to use different implementations of synchronisers in verification, and how we reason about class invariance properties in a concurrent setting. Further, we also show how the approach is suited to reason about programs using a different concurrency paradigm, namely kernel programs using the Single Instruction Multiple Data paradigm. Concretely, we illustrate how permission-based separation logic is suitable to verify functional correctness properties of OpenCL kernels. All verification techniques discussed in this paper are supported by the VerCors tool set.",
keywords = "EWI-24905, CR-D.2.4, Software Verification, EC Grant Agreement nr.: FP7/2007-2013, METIS-305942, EC Grant Agreement nr.: FP7/287767, VerCors tool, IR-91766, Concurrency, EC Grant Agreement nr.: FP7/258405",
author = "A. Amighi and Stefan Blom and Saeed Darabi and Marieke Huisman and Wojciech Mostowski and M. Zaharieva",
note = "eemcs-eprint-24905",
year = "2014",
month = "6",
doi = "10.1007/978-3-319-07317-0_5",
isbn = "978-3-319-07316-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
number = "8483",
pages = "172--216",
editor = "Marco Bernardo and Ferruccio Damiani and Reiner Hahnle and Einar Johnsen and Ina Schaefer",
booktitle = "Formal Methods for Executable Software Models - 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems",
address = "Germany",

}

Amighi, A, Blom, S, Darabi, S, Huisman, M, Mostowski, W & Zaharieva, M 2014, Verification of concurrent systems with VerCors. in M Bernardo, F Damiani, R Hahnle, E Johnsen & I Schaefer (eds), Formal Methods for Executable Software Models - 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems. Lecture Notes in Computer Science, no. 8483, vol. 8483, Springer Verlag, Berlin, pp. 172-216. DOI: 10.1007/978-3-319-07317-0_5

Verification of concurrent systems with VerCors. / Amighi, A.; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva, M.

Formal Methods for Executable Software Models - 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems. ed. / Marco Bernardo; Ferruccio Damiani; Reiner Hahnle; Einar Johnsen; Ina Schaefer. Berlin : Springer Verlag, 2014. p. 172-216 (Lecture Notes in Computer Science; Vol. 8483, No. 8483).

Research output: ScientificChapter

TY - CHAP

T1 - Verification of concurrent systems with VerCors

AU - Amighi,A.

AU - Blom,Stefan

AU - Darabi,Saeed

AU - Huisman,Marieke

AU - Mostowski,Wojciech

AU - Zaharieva,M.

N1 - eemcs-eprint-24905

PY - 2014/6

Y1 - 2014/6

N2 - This paper presents the VerCors approach to verification of concurrent software. It first discusses why verification of concurrent software is important, but also challenging. Then it shows how within the VerCors project we use permission-based separation logic to reason about multithreaded Java programs. We discuss in particular how we use the logic to use different implementations of synchronisers in verification, and how we reason about class invariance properties in a concurrent setting. Further, we also show how the approach is suited to reason about programs using a different concurrency paradigm, namely kernel programs using the Single Instruction Multiple Data paradigm. Concretely, we illustrate how permission-based separation logic is suitable to verify functional correctness properties of OpenCL kernels. All verification techniques discussed in this paper are supported by the VerCors tool set.

AB - This paper presents the VerCors approach to verification of concurrent software. It first discusses why verification of concurrent software is important, but also challenging. Then it shows how within the VerCors project we use permission-based separation logic to reason about multithreaded Java programs. We discuss in particular how we use the logic to use different implementations of synchronisers in verification, and how we reason about class invariance properties in a concurrent setting. Further, we also show how the approach is suited to reason about programs using a different concurrency paradigm, namely kernel programs using the Single Instruction Multiple Data paradigm. Concretely, we illustrate how permission-based separation logic is suitable to verify functional correctness properties of OpenCL kernels. All verification techniques discussed in this paper are supported by the VerCors tool set.

KW - EWI-24905

KW - CR-D.2.4

KW - Software Verification

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

KW - METIS-305942

KW - EC Grant Agreement nr.: FP7/287767

KW - VerCors tool

KW - IR-91766

KW - Concurrency

KW - EC Grant Agreement nr.: FP7/258405

U2 - 10.1007/978-3-319-07317-0_5

DO - 10.1007/978-3-319-07317-0_5

M3 - Chapter

SN - 978-3-319-07316-3

T3 - Lecture Notes in Computer Science

SP - 172

EP - 216

BT - Formal Methods for Executable Software Models - 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems

PB - Springer Verlag

ER -

Amighi A, Blom S, Darabi S, Huisman M, Mostowski W, Zaharieva M. Verification of concurrent systems with VerCors. In Bernardo M, Damiani F, Hahnle R, Johnsen E, Schaefer I, editors, Formal Methods for Executable Software Models - 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems. Berlin: Springer Verlag. 2014. p. 172-216. (Lecture Notes in Computer Science; 8483). Available from, DOI: 10.1007/978-3-319-07317-0_5