Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-38088-4_20
Title: Towards complete specifications with an error calculus
Authors: Le, Q.L.
Sharma, A.
Craciun, F.
Chin, W.-N. 
Issue Date: 2013
Citation: Le, Q.L.,Sharma, A.,Craciun, F.,Chin, W.-N. (2013). Towards complete specifications with an error calculus. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 7871 LNCS : 291-306. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-38088-4_20
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. © 2013 Springer-Verlag.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/78400
ISBN: 9783642380877
ISSN: 03029743
DOI: 10.1007/978-3-642-38088-4_20
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.