Towards complete specifications with an error calculus

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

doi:10.1007/978-3-642-38088-4_20

Towards complete specifications with an error calculus

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

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	NASA Formal Methods - 5th International Symposium, NFM 2013, Proceedings
Pages	291-306
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-38088-4_20
Publication status	Published - 9 Sept 2013
Event	5th International Symposium on NASA Formal Methods - Moffett Field, CA, United States Duration: 14 May 2013 → 16 May 2013

Publication series

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

Conference

Conference	5th International Symposium on NASA Formal Methods
Abbreviated title	NFM 2013
Country/Territory	United States
City	Moffett Field, CA
Period	14/05/13 → 16/05/13

Access to Document

10.1007/978-3-642-38088-4_20

Cite this

Le, Q. L., Sharma, A., Craciun, F., & Chin, W. N. (2013). Towards complete specifications with an error calculus. In NASA Formal Methods - 5th International Symposium, NFM 2013, Proceedings (pp. 291-306). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7871 LNCS). https://doi.org/10.1007/978-3-642-38088-4_20

@inproceedings{61c7f11e167b4fe79ab5d34d2508f0b7,

title = "Towards complete specifications with an error calculus",

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.",

author = "Le, {Quang Loc} and Asankhaya Sharma and Florin Craciun and Chin, {Wei Ngan}",

year = "2013",

month = sep,

day = "9",

doi = "10.1007/978-3-642-38088-4_20",

language = "English",

isbn = "9783642380877",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "291--306",

booktitle = "NASA Formal Methods - 5th International Symposium, NFM 2013, Proceedings",

note = "5th International Symposium on NASA Formal Methods, NFM 2013 ; Conference date: 14-05-2013 Through 16-05-2013",

}

Le, QL, Sharma, A, Craciun, F & Chin, WN 2013, Towards complete specifications with an error calculus. in NASA Formal Methods - 5th International Symposium, NFM 2013, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7871 LNCS, pp. 291-306, 5th International Symposium on NASA Formal Methods, Moffett Field, CA, United States, 14/05/13. https://doi.org/10.1007/978-3-642-38088-4_20

Towards complete specifications with an error calculus. / Le, Quang Loc; Sharma, Asankhaya; Craciun, Florin et al.
NASA Formal Methods - 5th International Symposium, NFM 2013, Proceedings. 2013. p. 291-306 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7871 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Towards complete specifications with an error calculus

AU - Le, Quang Loc

AU - Sharma, Asankhaya

AU - Craciun, Florin

AU - Chin, Wei Ngan

PY - 2013/9/9

Y1 - 2013/9/9

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84883335630&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-38088-4_20

DO - 10.1007/978-3-642-38088-4_20

M3 - Conference contribution

AN - SCOPUS:84883335630

SN - 9783642380877

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 291

EP - 306

BT - NASA Formal Methods - 5th International Symposium, NFM 2013, Proceedings

T2 - 5th International Symposium on NASA Formal Methods

Y2 - 14 May 2013 through 16 May 2013

ER -

Towards complete specifications with an error calculus

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this