Verification of concurrent systems with VerCors

Afshin Amighi, Stefan Blom, Saeed Darabi, Marieke Huisman, Wojciech Mostowski, Marina Zaharieva-Stojanovski

Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

6 Citations (Scopus)
16 Downloads (Pure)

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 languageEnglish
Title of host publicationFormal Methods for Executable Software Models
Subtitle of host publication14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems
EditorsMarco Bernardo, Ferruccio Damiani, Reiner Hähnle, Einar Broch Johnsen, Ina Schaefer
Place of PublicationCham
PublisherSpringer
Pages172-216
Number of pages45
ISBN (Electronic)978-3-319-07317-0
ISBN (Print)978-3-319-07316-3
DOIs
Publication statusPublished - Jun 2014
Event14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014 - Bertinoro, Italy
Duration: 16 Jun 201420 Jun 2014
Conference number: 14

Publication series

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

Conference

Conference14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014
Abbreviated titleSFM
CountryItaly
CityBertinoro
Period16/06/1420/06/14

Fingerprint

Invariance

Keywords

  • EC Grant Agreement nr.: FP7/287767
  • EC Grant Agreement nr.: FP7/2007-2013
  • EC Grant Agreement nr.: FP7/258405
  • CR-D.2.4
  • Global memory
  • Software verification
  • VerCors tool
  • Concurrency
  • Concurrent program
  • Concurrent system
  • Java modeling language
  • Class invariants

Cite this

Amighi, A., Blom, S., Darabi, S., Huisman, M., Mostowski, W., & Zaharieva-Stojanovski, M. (2014). Verification of concurrent systems with VerCors. In M. Bernardo, F. Damiani, R. Hähnle, E. Broch 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). Cham: Springer. https://doi.org/10.1007/978-3-319-07317-0_5
Amighi, Afshin ; Blom, Stefan ; Darabi, Saeed ; Huisman, Marieke ; Mostowski, Wojciech ; Zaharieva-Stojanovski, Marina. / 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. editor / Marco Bernardo ; Ferruccio Damiani ; Reiner Hähnle ; Einar Broch Johnsen ; Ina Schaefer. Cham : Springer, 2014. pp. 172-216 (Lecture Notes in Computer Science).
@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 = "EC Grant Agreement nr.: FP7/287767, EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/258405, CR-D.2.4, Global memory, Software verification, VerCors tool, Concurrency, Concurrent program, Concurrent system, Java modeling language, Class invariants",
author = "Afshin Amighi and Stefan Blom and Saeed Darabi and Marieke Huisman and Wojciech Mostowski and Marina Zaharieva-Stojanovski",
year = "2014",
month = "6",
doi = "10.1007/978-3-319-07317-0_5",
language = "English",
isbn = "978-3-319-07316-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "172--216",
editor = "Marco Bernardo and Ferruccio Damiani and Reiner H{\"a}hnle and { Broch Johnsen}, Einar and Ina Schaefer",
booktitle = "Formal Methods for Executable Software Models",

}

Amighi, A, Blom, S, Darabi, S, Huisman, M, Mostowski, W & Zaharieva-Stojanovski, M 2014, Verification of concurrent systems with VerCors. in M Bernardo, F Damiani, R Hähnle, E Broch 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, vol. 8483, Springer, Cham, pp. 172-216, 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014, Bertinoro, Italy, 16/06/14. https://doi.org/10.1007/978-3-319-07317-0_5

Verification of concurrent systems with VerCors. / Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina.

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 Hähnle; Einar Broch Johnsen; Ina Schaefer. Cham : Springer, 2014. p. 172-216 (Lecture Notes in Computer Science; Vol. 8483).

Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

TY - CHAP

T1 - Verification of concurrent systems with VerCors

AU - Amighi, Afshin

AU - Blom, Stefan

AU - Darabi, Saeed

AU - Huisman, Marieke

AU - Mostowski, Wojciech

AU - Zaharieva-Stojanovski, Marina

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 - EC Grant Agreement nr.: FP7/287767

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

KW - EC Grant Agreement nr.: FP7/258405

KW - CR-D.2.4

KW - Global memory

KW - Software verification

KW - VerCors tool

KW - Concurrency

KW - Concurrent program

KW - Concurrent system

KW - Java modeling language

KW - Class invariants

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

A2 - Bernardo, Marco

A2 - Damiani, Ferruccio

A2 - Hähnle, Reiner

A2 - Broch Johnsen, Einar

A2 - Schaefer, Ina

PB - Springer

CY - Cham

ER -

Amighi A, Blom S, Darabi S, Huisman M, Mostowski W, Zaharieva-Stojanovski M. Verification of concurrent systems with VerCors. In Bernardo M, Damiani F, Hähnle R, Broch 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. Cham: Springer. 2014. p. 172-216. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-07317-0_5