Static Code Verification Through Process Models

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

11 Downloads (Pure)

Abstract

In this extended abstract, we combine two techniques for program verification: one is Hoare-style static verification, and the other is model checking of state transition systems. We relate the two techniques semantically through the use of a ghost variable. Actions that are performed by the program can be logged into this variable, building an event structure as its value. We require the event structure to grow incrementally by construction, giving it behavior suitable for model checking. Invariants specify a correspondence between the event structure and the program state. The combined power of model checking and static code verification with separation logic based reasoning, gives a new and intuitive way to do program verification. We describe our idea in a tool-agnostic way: we do not give implementation details, nor do we assume that the static verification tool to which our idea might apply is implemented in a particular way.
Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation. Distributed Systems
Subtitle of host publication8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III
EditorsTiziana Margaria, Bernhard Steffen
Place of PublicationCham
PublisherSpringer
Pages343-354
Number of pages12
ISBN (Electronic)978-3-030-03424-5
ISBN (Print)978-3-030-03423-8
DOIs
Publication statusPublished - 31 Oct 2018
Event8th International Symposium, ISoLA 2018 - Royal Apollonia Beach Hotel, Limassol, Cyprus
Duration: 5 Nov 20189 Nov 2018
Conference number: 8
http://www.isola-conference.org/isola2018/

Publication series

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

Conference

Conference8th International Symposium, ISoLA 2018
Abbreviated titleISoLA 2018
CountryCyprus
CityLimassol
Period5/11/189/11/18
Internet address

Fingerprint

Model checking

Cite this

Joosten, S. J. C., & Huisman, M. (2018). Static Code Verification Through Process Models. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III (pp. 343-354). (Lecture Notes in Computer Science; Vol. 11246). Cham: Springer. https://doi.org/10.1007/978-3-030-03424-5_23
Joosten, Sebastiaan J. C. ; Huisman, Marieke. / Static Code Verification Through Process Models. Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III. editor / Tiziana Margaria ; Bernhard Steffen. Cham : Springer, 2018. pp. 343-354 (Lecture Notes in Computer Science).
@inproceedings{233aeb9562a3494aa6ee6f5df582ee99,
title = "Static Code Verification Through Process Models",
abstract = "In this extended abstract, we combine two techniques for program verification: one is Hoare-style static verification, and the other is model checking of state transition systems. We relate the two techniques semantically through the use of a ghost variable. Actions that are performed by the program can be logged into this variable, building an event structure as its value. We require the event structure to grow incrementally by construction, giving it behavior suitable for model checking. Invariants specify a correspondence between the event structure and the program state. The combined power of model checking and static code verification with separation logic based reasoning, gives a new and intuitive way to do program verification. We describe our idea in a tool-agnostic way: we do not give implementation details, nor do we assume that the static verification tool to which our idea might apply is implemented in a particular way.",
author = "Joosten, {Sebastiaan J. C.} and Marieke Huisman",
year = "2018",
month = "10",
day = "31",
doi = "10.1007/978-3-030-03424-5_23",
language = "English",
isbn = "978-3-030-03423-8",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "343--354",
editor = "Tiziana Margaria and Bernhard Steffen",
booktitle = "Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems",

}

Joosten, SJC & Huisman, M 2018, Static Code Verification Through Process Models. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III. Lecture Notes in Computer Science, vol. 11246, Springer, Cham, pp. 343-354, 8th International Symposium, ISoLA 2018, Limassol, Cyprus, 5/11/18. https://doi.org/10.1007/978-3-030-03424-5_23

Static Code Verification Through Process Models. / Joosten, Sebastiaan J. C.; Huisman, Marieke.

Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III. ed. / Tiziana Margaria; Bernhard Steffen. Cham : Springer, 2018. p. 343-354 (Lecture Notes in Computer Science; Vol. 11246).

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

TY - GEN

T1 - Static Code Verification Through Process Models

AU - Joosten, Sebastiaan J. C.

AU - Huisman, Marieke

PY - 2018/10/31

Y1 - 2018/10/31

N2 - In this extended abstract, we combine two techniques for program verification: one is Hoare-style static verification, and the other is model checking of state transition systems. We relate the two techniques semantically through the use of a ghost variable. Actions that are performed by the program can be logged into this variable, building an event structure as its value. We require the event structure to grow incrementally by construction, giving it behavior suitable for model checking. Invariants specify a correspondence between the event structure and the program state. The combined power of model checking and static code verification with separation logic based reasoning, gives a new and intuitive way to do program verification. We describe our idea in a tool-agnostic way: we do not give implementation details, nor do we assume that the static verification tool to which our idea might apply is implemented in a particular way.

AB - In this extended abstract, we combine two techniques for program verification: one is Hoare-style static verification, and the other is model checking of state transition systems. We relate the two techniques semantically through the use of a ghost variable. Actions that are performed by the program can be logged into this variable, building an event structure as its value. We require the event structure to grow incrementally by construction, giving it behavior suitable for model checking. Invariants specify a correspondence between the event structure and the program state. The combined power of model checking and static code verification with separation logic based reasoning, gives a new and intuitive way to do program verification. We describe our idea in a tool-agnostic way: we do not give implementation details, nor do we assume that the static verification tool to which our idea might apply is implemented in a particular way.

U2 - 10.1007/978-3-030-03424-5_23

DO - 10.1007/978-3-030-03424-5_23

M3 - Conference contribution

SN - 978-3-030-03423-8

T3 - Lecture Notes in Computer Science

SP - 343

EP - 354

BT - Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer

CY - Cham

ER -

Joosten SJC, Huisman M. Static Code Verification Through Process Models. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III. Cham: Springer. 2018. p. 343-354. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-03424-5_23