Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
Towards Complete Specifications with an Error Calculus
verfasst von : Quang Loc Le, Asankhaya Sharma, Florin Craciun, Wei-Ngan Chin
Erschienen in: NASA Formal Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.