Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools

Reiner Hähnle; Marieke Huisman

doi:10.1007/978-3-319-91908-9_18

Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools

Reiner Hähnle^*, Marieke Huisman

^*Corresponding author for this work

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

27 Citations (Scopus)

1 Downloads (Pure)

Abstract

Deductive software verification aims at formally verifying that all possible behaviors of a given program satisfy formally defined, possibly complex properties, where the verification process is based on logical inference. We follow the trajectory of the field from its inception in the late 1960s via its current state to its promises for the future, from pen-and-paper proofs for programs written in small, idealized languages to highly automated proofs of complex library or system code written in mainstream languages. We take stock of the state-of-art and give a list of the most important challenges for the further development of the field of deductive software verification.

Original language	English
Title of host publication	Computing and Software Science
Subtitle of host publication	State of the Art and Perspectives
Editors	Bernhard Steffen, Gerhard Woeginger
Place of Publication	Cham
Publisher	Springer
Pages	345-373
Number of pages	29
ISBN (Electronic)	978-3-319-91908-9
ISBN (Print)	978-3-319-91907-2
DOIs	https://doi.org/10.1007/978-3-319-91908-9_18
Publication status	Published - 2019

Publication series

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

Name	Theoretical Computer Science and General Issues
Publisher	Springer

Access to Document

10.1007/978-3-319-91908-9_18

Cite this

Hähnle, R., & Huisman, M. (2019). Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools. In B. Steffen, & G. Woeginger (Eds.), Computing and Software Science : State of the Art and Perspectives (pp. 345-373). (Lecture Notes in Computer Science; Vol. 10000), (Theoretical Computer Science and General Issues). Springer. https://doi.org/10.1007/978-3-319-91908-9_18

@inbook{34e7beecf4454c0bac5684a16ea3605e,

title = "Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools",

abstract = "Deductive software verification aims at formally verifying that all possible behaviors of a given program satisfy formally defined, possibly complex properties, where the verification process is based on logical inference. We follow the trajectory of the field from its inception in the late 1960s via its current state to its promises for the future, from pen-and-paper proofs for programs written in small, idealized languages to highly automated proofs of complex library or system code written in mainstream languages. We take stock of the state-of-art and give a list of the most important challenges for the further development of the field of deductive software verification.",

author = "Reiner H{\"a}hnle and Marieke Huisman",

year = "2019",

doi = "10.1007/978-3-319-91908-9_18",

language = "English",

isbn = "978-3-319-91907-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "345--373",

editor = "Bernhard Steffen and Gerhard Woeginger",

booktitle = "Computing and Software Science",

}

Hähnle, R & Huisman, M 2019, Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools. in B Steffen & G Woeginger (eds), Computing and Software Science : State of the Art and Perspectives. Lecture Notes in Computer Science, vol. 10000, Theoretical Computer Science and General Issues, Springer, Cham, pp. 345-373. https://doi.org/10.1007/978-3-319-91908-9_18

Deductive Software Verification : From Pen-and-Paper Proofs to Industrial Tools. / Hähnle, Reiner; Huisman, Marieke.

Computing and Software Science : State of the Art and Perspectives. ed. / Bernhard Steffen; Gerhard Woeginger. Cham : Springer, 2019. p. 345-373 (Lecture Notes in Computer Science; Vol. 10000), (Theoretical Computer Science and General Issues).

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

TY - CHAP

T1 - Deductive Software Verification

T2 - From Pen-and-Paper Proofs to Industrial Tools

AU - Hähnle, Reiner

AU - Huisman, Marieke

PY - 2019

Y1 - 2019

N2 - Deductive software verification aims at formally verifying that all possible behaviors of a given program satisfy formally defined, possibly complex properties, where the verification process is based on logical inference. We follow the trajectory of the field from its inception in the late 1960s via its current state to its promises for the future, from pen-and-paper proofs for programs written in small, idealized languages to highly automated proofs of complex library or system code written in mainstream languages. We take stock of the state-of-art and give a list of the most important challenges for the further development of the field of deductive software verification.

AB - Deductive software verification aims at formally verifying that all possible behaviors of a given program satisfy formally defined, possibly complex properties, where the verification process is based on logical inference. We follow the trajectory of the field from its inception in the late 1960s via its current state to its promises for the future, from pen-and-paper proofs for programs written in small, idealized languages to highly automated proofs of complex library or system code written in mainstream languages. We take stock of the state-of-art and give a list of the most important challenges for the further development of the field of deductive software verification.

U2 - 10.1007/978-3-319-91908-9_18

DO - 10.1007/978-3-319-91908-9_18

M3 - Chapter

SN - 978-3-319-91907-2

T3 - Lecture Notes in Computer Science

SP - 345

EP - 373

BT - Computing and Software Science

A2 - Steffen, Bernhard

A2 - Woeginger, Gerhard

PB - Springer

CY - Cham

ER -

Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools

Abstract

Publication series

Access to Document

Fingerprint

Cite this