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

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

1 Citation (Scopus)
7 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 languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation. Modeling
Subtitle of host publication8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I
EditorsTiziana Margaria, Bernhard Steffen
Place of PublicationCham
PublisherSpringer
Pages111-118
Number of pages8
ISBN (Electronic)978-3-030-03418-4
ISBN (Print)978-3-030-03417-7
DOIs
Publication statusPublished - 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
Volume11244
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

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). Cham: 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.",
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",

}

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 proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - On Models and Code

T2 - A Unified Approach to Support Large-Scale Deductive Program Verification

AU - Huisman, Marieke

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.

UR - http://www.scopus.com/inward/record.url?scp=85056476794&partnerID=8YFLogxK

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

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). https://doi.org/10.1007/978-3-030-03418-4_7