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 proceedingChapterAcademicpeer-review

    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 languageEnglish
    Title of host publicationComputing and Software Science
    Subtitle of host publicationState of the Art and Perspectives
    EditorsBernhard Steffen, Gerhard Woeginger
    Place of PublicationCham
    PublisherSpringer
    Pages345-373
    Number of pages29
    ISBN (Electronic)978-3-319-91908-9
    ISBN (Print)978-3-319-91907-2
    DOIs
    Publication statusPublished - 2019

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume10000
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349
    NameTheoretical Computer Science and General Issues
    PublisherSpringer

    Fingerprint

    Trajectories

    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). Cham: Springer. https://doi.org/10.1007/978-3-319-91908-9_18
    Hähnle, Reiner ; Huisman, Marieke. / Deductive Software Verification : From Pen-and-Paper Proofs to Industrial Tools. Computing and Software Science : State of the Art and Perspectives. editor / Bernhard Steffen ; Gerhard Woeginger. Cham : Springer, 2019. pp. 345-373 (Lecture Notes in Computer Science). (Theoretical Computer Science and General Issues).
    @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 proceedingChapterAcademicpeer-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 -

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