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

    3 Citations (Scopus)

    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 Dive into the research topics of 'Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools'. Together they form a unique fingerprint.

    Cite this