Please use this identifier to cite or link to this item:
https://doi.org/10.1007/978-3-642-38088-4_20
| DC Field | Value | |
|---|---|---|
| dc.title | Towards complete specifications with an error calculus | |
| dc.contributor.author | Le, Q.L. | |
| dc.contributor.author | Sharma, A. | |
| dc.contributor.author | Craciun, F. | |
| dc.contributor.author | Chin, W.-N. | |
| dc.date.accessioned | 2014-07-04T03:15:50Z | |
| dc.date.available | 2014-07-04T03:15:50Z | |
| dc.date.issued | 2013 | |
| dc.identifier.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. <a href="https://doi.org/10.1007/978-3-642-38088-4_20" target="_blank">https://doi.org/10.1007/978-3-642-38088-4_20</a> | |
| dc.identifier.isbn | 9783642380877 | |
| dc.identifier.issn | 03029743 | |
| dc.identifier.uri | http://scholarbank.nus.edu.sg/handle/10635/78400 | |
| dc.description.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. | |
| dc.description.uri | http://libproxy1.nus.edu.sg/login?url=http://dx.doi.org/10.1007/978-3-642-38088-4_20 | |
| dc.source | Scopus | |
| dc.type | Conference Paper | |
| dc.contributor.department | COMPUTER SCIENCE | |
| dc.description.doi | 10.1007/978-3-642-38088-4_20 | |
| dc.description.sourcetitle | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | |
| dc.description.volume | 7871 LNCS | |
| dc.description.page | 291-306 | |
| dc.identifier.isiut | NOT_IN_WOS | |
| Appears in Collections: | Staff Publications | |
Show simple item record
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.