Verification of concurrent systems with VerCors

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

doi:10.1007/978-3-319-07317-0_5

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 proceeding › Chapter › Academic

14 Citations (Scopus)

27 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 language	English
Title of host publication	Formal Methods for Executable Software Models
Subtitle of host publication	14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems
Editors	Marco Bernardo, Ferruccio Damiani, Reiner Hähnle, Einar Broch Johnsen, Ina Schaefer
Place of Publication	Cham
Publisher	Springer
Pages	172-216
Number of pages	45
ISBN (Electronic)	978-3-319-07317-0
ISBN (Print)	978-3-319-07316-3
DOIs	https://doi.org/10.1007/978-3-319-07317-0_5
Publication status	Published - Jun 2014
Event	14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014 - Bertinoro, Italy Duration: 16 Jun 2014 → 20 Jun 2014 Conference number: 14

Publication series

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

Conference

Conference	14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014
Abbreviated title	SFM
Country/Territory	Italy
City	Bertinoro
Period	16/06/14 → 20/06/14

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

Access to Document

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

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). Springer. https://doi.org/10.1007/978-3-319-07317-0_5

Amighi, Afshin ; Blom, Stefan ; Darabi, Saeed et al. / 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 = jun,

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

address = "Germany",

note = "14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014, SFM ; Conference date: 16-06-2014 Through 20-06-2014",

}

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 et al.
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 proceeding › Chapter › Academic

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

N1 - Conference code: 14

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

T2 - 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014

Y2 - 16 June 2014 through 20 June 2014

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). doi: 10.1007/978-3-319-07317-0_5

Verification of concurrent systems with VerCors

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this