On Models and Code: A Unified Approach to Support Large-Scale Deductive Program Verification

Marieke Huisman

doi:10.1007/978-3-030-03418-4_7

On Models and Code: A Unified Approach to Support Large-Scale Deductive Program Verification

Marieke Huisman

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

1 Citation (Scopus)

213 Downloads (Pure)

Abstract

Despite the substantial progress in the area of deductive program verification over the last years, it still remains a challenge to use deductive verification on large-scale industrial applications. In this abstract, I analyse why this is case, and I argue that in order to solve this, we need to soften the border between models and code. This has two important advantages: (1) it would make it easier to reason about high-level behaviour of programs, using deductive verification, and (2) it would allow to reason about incomplete applications during the development process. I discuss how the first steps towards this goal are supported by verification techniques within the VerCors project, and I will sketch the future steps that are necessary to realise this goal.

Original language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation. Modeling
Subtitle of host publication	8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I
Editors	Tiziana Margaria, Bernhard Steffen
Place of Publication	Cham
Publisher	Springer
Pages	111-118
Number of pages	8
ISBN (Electronic)	978-3-030-03418-4
ISBN (Print)	978-3-030-03417-7
DOIs	https://doi.org/10.1007/978-3-030-03418-4_7
Publication status	Published - 2018
Event	8th International Symposium, ISoLA 2018 - Royal Apollonia Beach Hotel, Limassol, Cyprus Duration: 5 Nov 2018 → 9 Nov 2018 Conference number: 8 http://www.isola-conference.org/isola2018/

Publication series

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

Conference

Conference	8th International Symposium, ISoLA 2018
Abbreviated title	ISoLA 2018
Country/Territory	Cyprus
City	Limassol
Period	5/11/18 → 9/11/18
Internet address	http://www.isola-conference.org/isola2018/

Keywords

2019 OA procedure

Access to Document

10.1007/978-3-030-03418-4_7

Huisman2018_Chapter_OnModelsAndCodeFinal published version, 344 KBLicence: Taverne

Cite this

Huisman, M. (2018). On Models and Code: A Unified Approach to Support Large-Scale Deductive Program Verification. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I (pp. 111-118). (Lecture Notes in Computer Science; Vol. 11244). Springer. https://doi.org/10.1007/978-3-030-03418-4_7

Huisman, Marieke. / On Models and Code : A Unified Approach to Support Large-Scale Deductive Program Verification. Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I. editor / Tiziana Margaria ; Bernhard Steffen. Cham : Springer, 2018. pp. 111-118 (Lecture Notes in Computer Science).

@inproceedings{e00e7414f3474e0cb69ec6119213a8d7,

title = "On Models and Code: A Unified Approach to Support Large-Scale Deductive Program Verification",

abstract = "Despite the substantial progress in the area of deductive program verification over the last years, it still remains a challenge to use deductive verification on large-scale industrial applications. In this abstract, I analyse why this is case, and I argue that in order to solve this, we need to soften the border between models and code. This has two important advantages: (1) it would make it easier to reason about high-level behaviour of programs, using deductive verification, and (2) it would allow to reason about incomplete applications during the development process. I discuss how the first steps towards this goal are supported by verification techniques within the VerCors project, and I will sketch the future steps that are necessary to realise this goal.",

keywords = "2019 OA procedure",

author = "Marieke Huisman",

year = "2018",

doi = "10.1007/978-3-030-03418-4\_7",

language = "English",

isbn = "978-3-030-03417-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "111--118",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation. Modeling",

address = "Germany",

note = "8th International Symposium, ISoLA 2018, ISoLA 2018 ; Conference date: 05-11-2018 Through 09-11-2018",

url = "http://www.isola-conference.org/isola2018/",

}

Huisman, M 2018, On Models and Code: A Unified Approach to Support Large-Scale Deductive Program Verification. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11244, Springer, Cham, pp. 111-118, 8th International Symposium, ISoLA 2018, Limassol, Cyprus, 5/11/18. https://doi.org/10.1007/978-3-030-03418-4_7

On Models and Code: A Unified Approach to Support Large-Scale Deductive Program Verification. / Huisman, Marieke.
Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I. ed. / Tiziana Margaria; Bernhard Steffen. Cham: Springer, 2018. p. 111-118 (Lecture Notes in Computer Science; Vol. 11244).

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

TY - GEN

T1 - On Models and Code

T2 - 8th International Symposium, ISoLA 2018

AU - Huisman, Marieke

N1 - Conference code: 8

PY - 2018

Y1 - 2018

N2 - Despite the substantial progress in the area of deductive program verification over the last years, it still remains a challenge to use deductive verification on large-scale industrial applications. In this abstract, I analyse why this is case, and I argue that in order to solve this, we need to soften the border between models and code. This has two important advantages: (1) it would make it easier to reason about high-level behaviour of programs, using deductive verification, and (2) it would allow to reason about incomplete applications during the development process. I discuss how the first steps towards this goal are supported by verification techniques within the VerCors project, and I will sketch the future steps that are necessary to realise this goal.

AB - Despite the substantial progress in the area of deductive program verification over the last years, it still remains a challenge to use deductive verification on large-scale industrial applications. In this abstract, I analyse why this is case, and I argue that in order to solve this, we need to soften the border between models and code. This has two important advantages: (1) it would make it easier to reason about high-level behaviour of programs, using deductive verification, and (2) it would allow to reason about incomplete applications during the development process. I discuss how the first steps towards this goal are supported by verification techniques within the VerCors project, and I will sketch the future steps that are necessary to realise this goal.

KW - 2019 OA procedure

UR - https://www.scopus.com/pages/publications/85056476794

U2 - 10.1007/978-3-030-03418-4_7

DO - 10.1007/978-3-030-03418-4_7

M3 - Conference contribution

SN - 978-3-030-03417-7

T3 - Lecture Notes in Computer Science

SP - 111

EP - 118

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

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer

CY - Cham

Y2 - 5 November 2018 through 9 November 2018

ER -

Huisman M. On Models and Code: A Unified Approach to Support Large-Scale Deductive Program Verification. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I. Cham: Springer. 2018. p. 111-118. (Lecture Notes in Computer Science). Epub 2018 Oct 29. doi: 10.1007/978-3-030-03418-4_7

On Models and Code: A Unified Approach to Support Large-Scale Deductive Program Verification

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this