Dynamic Frames Based Verification Method for Concurrent Java Programs

Wojciech Mostowski

doi:10.1007/978-3-319-29613-5_8

Dynamic Frames Based Verification Method for Concurrent Java Programs

Wojciech Mostowski

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

4 Citations (Scopus)

123 Downloads (Pure)

Abstract

In this paper we discuss a verification method for concurrent Java programs based on the concept of dynamic frames. We build on our earlier work that proposes a new, symbolic permission system for concurrent reasoning and we provide the following new contributions. First, we describe our approach for proving program specifications to be self-framed w.r.t. permissions, which is a necessary condition to maintain soundness in concurrent reasoning. Second, we show how we use predicates to provide modular and reusable specifications for program synchronisation points, like locks or forked threads. Our work primarily targets the KeY verification system with its specification language JML* and symbolic execution proving method. Hence, we also give the current status of the work on implementation and we discuss some examples that are verifiable with KeY.

Original language	English
Title of host publication	Proceedings of the 7th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2015. Revised Selected Papers
Editors	Arie Gurfinkel, Sanjit A. Seshia
Place of Publication	Cham
Publisher	Springer
Pages	124-141
Number of pages	18
ISBN (Electronic)	978-3-319-29613-5
ISBN (Print)	978-3-319-29612-8
DOIs	https://doi.org/10.1007/978-3-319-29613-5_8
Publication status	Published - 2016
Event	7th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2015 - San Francisco, United States Duration: 18 Jul 2015 → 19 Jul 2015 Conference number: 7

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer International Publishing Switzerland
Volume	9593
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	7th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2015
Abbreviated title	VSTTE
Country/Territory	United States
City	San Francisco
Period	18/07/15 → 19/07/15

Keywords

JML
Java
Dynamic frames
Interactive verification
Symbolic permissions
Permission accounting

Access to Document

10.1007/978-3-319-29613-5_8

Mostowski2016dynamicAccepted author version, 419 KB

Cite this

Mostowski, W. (2016). Dynamic Frames Based Verification Method for Concurrent Java Programs. In A. Gurfinkel, & S. A. Seshia (Eds.), Proceedings of the 7th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2015. Revised Selected Papers (pp. 124-141). (Lecture Notes in Computer Science; Vol. 9593). Springer. https://doi.org/10.1007/978-3-319-29613-5_8

@inproceedings{b9d0e559252e40b8b01dc7334a9fb061,

title = "Dynamic Frames Based Verification Method for Concurrent Java Programs",

abstract = "In this paper we discuss a verification method for concurrent Java programs based on the concept of dynamic frames. We build on our earlier work that proposes a new, symbolic permission system for concurrent reasoning and we provide the following new contributions. First, we describe our approach for proving program specifications to be self-framed w.r.t. permissions, which is a necessary condition to maintain soundness in concurrent reasoning. Second, we show how we use predicates to provide modular and reusable specifications for program synchronisation points, like locks or forked threads. Our work primarily targets the KeY verification system with its specification language JML* and symbolic execution proving method. Hence, we also give the current status of the work on implementation and we discuss some examples that are verifiable with KeY.",

keywords = "JML, Java, Dynamic frames, Interactive verification, Symbolic permissions, Permission accounting",

author = "Wojciech Mostowski",

year = "2016",

doi = "10.1007/978-3-319-29613-5_8",

language = "English",

isbn = "978-3-319-29612-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "124--141",

editor = "Arie Gurfinkel and Seshia, {Sanjit A.}",

booktitle = "Proceedings of the 7th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2015. Revised Selected Papers",

note = "7th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2015, VSTTE ; Conference date: 18-07-2015 Through 19-07-2015",

}

Mostowski, W 2016, Dynamic Frames Based Verification Method for Concurrent Java Programs. in A Gurfinkel & SA Seshia (eds), Proceedings of the 7th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2015. Revised Selected Papers. Lecture Notes in Computer Science, vol. 9593, Springer, Cham, pp. 124-141, 7th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2015, San Francisco, California, United States, 18/07/15. https://doi.org/10.1007/978-3-319-29613-5_8

Dynamic Frames Based Verification Method for Concurrent Java Programs. / Mostowski, Wojciech.

Proceedings of the 7th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2015. Revised Selected Papers. ed. / Arie Gurfinkel; Sanjit A. Seshia. Cham : Springer, 2016. p. 124-141 (Lecture Notes in Computer Science; Vol. 9593).

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

TY - GEN

T1 - Dynamic Frames Based Verification Method for Concurrent Java Programs

AU - Mostowski, Wojciech

N1 - Conference code: 7

PY - 2016

Y1 - 2016

N2 - In this paper we discuss a verification method for concurrent Java programs based on the concept of dynamic frames. We build on our earlier work that proposes a new, symbolic permission system for concurrent reasoning and we provide the following new contributions. First, we describe our approach for proving program specifications to be self-framed w.r.t. permissions, which is a necessary condition to maintain soundness in concurrent reasoning. Second, we show how we use predicates to provide modular and reusable specifications for program synchronisation points, like locks or forked threads. Our work primarily targets the KeY verification system with its specification language JML* and symbolic execution proving method. Hence, we also give the current status of the work on implementation and we discuss some examples that are verifiable with KeY.

AB - In this paper we discuss a verification method for concurrent Java programs based on the concept of dynamic frames. We build on our earlier work that proposes a new, symbolic permission system for concurrent reasoning and we provide the following new contributions. First, we describe our approach for proving program specifications to be self-framed w.r.t. permissions, which is a necessary condition to maintain soundness in concurrent reasoning. Second, we show how we use predicates to provide modular and reusable specifications for program synchronisation points, like locks or forked threads. Our work primarily targets the KeY verification system with its specification language JML* and symbolic execution proving method. Hence, we also give the current status of the work on implementation and we discuss some examples that are verifiable with KeY.

KW - JML

KW - Java

KW - Dynamic frames

KW - Interactive verification

KW - Symbolic permissions

KW - Permission accounting

U2 - 10.1007/978-3-319-29613-5_8

DO - 10.1007/978-3-319-29613-5_8

M3 - Conference contribution

SN - 978-3-319-29612-8

T3 - Lecture Notes in Computer Science

SP - 124

EP - 141

BT - Proceedings of the 7th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2015. Revised Selected Papers

A2 - Gurfinkel, Arie

A2 - Seshia, Sanjit A.

PB - Springer

CY - Cham

T2 - 7th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2015

Y2 - 18 July 2015 through 19 July 2015

ER -

Dynamic Frames Based Verification Method for Concurrent Java Programs

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this