Towards complete specifications with an error calculus

Quang Loc Le, Asankhaya Sharma, Florin Craciun, Wei Ngan Chin

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    3 Citations (Scopus)

    Abstract

    We present an error calculus to support a novel specification mechanism for sound and/or complete safety properties that are to be given by users. With such specifications, our calculus can form a foundation for both proving program safety and/or discovering real bugs. The basis of our calculus is an algebra with a lattice domain of four abstract statuses (namely unreachability, validity, must-error and may-error) on possible program states and four operators for this domain to calculate suitable program status.We show how proof search and error localization can be supported by our calculus. Our calculus can also be extended to separation logic with support for user-defined predicates and lemmas.We have implemented our calculus in an automated verification tool for pointer-based programs. Initial experiments have confirmed that it can achieve the dual objectives, namely of safety proving and bug finding, with modest overheads.

    Original languageEnglish
    Title of host publicationNASA Formal Methods - 5th International Symposium, NFM 2013, Proceedings
    Pages291-306
    Number of pages16
    DOIs
    Publication statusPublished - 9 Sep 2013
    Event5th International Symposium on NASA Formal Methods - Moffett Field, CA, United States
    Duration: 14 May 201316 May 2013

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume7871 LNCS
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference5th International Symposium on NASA Formal Methods
    Abbreviated titleNFM 2013
    Country/TerritoryUnited States
    CityMoffett Field, CA
    Period14/05/1316/05/13

    Fingerprint

    Dive into the research topics of 'Towards complete specifications with an error calculus'. Together they form a unique fingerprint.

    Cite this