Please use this identifier to cite or link to this item:
https://doi.org/10.1007/978-3-319-03542-0_8
DC Field | Value | |
---|---|---|
dc.title | Bi-abduction with pure properties for specification inference | |
dc.contributor.author | Trinh, M.-T. | |
dc.contributor.author | Loc, Q. | |
dc.contributor.author | David, C. | |
dc.contributor.author | Chin, W.-N. | |
dc.date.accessioned | 2014-07-04T03:11:46Z | |
dc.date.available | 2014-07-04T03:11:46Z | |
dc.date.issued | 2013 | |
dc.identifier.citation | Trinh, M.-T.,Loc, Q.,David, C.,Chin, W.-N. (2013). Bi-abduction with pure properties for specification inference. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 8301 LNCS : 107-123. ScholarBank@NUS Repository. <a href="https://doi.org/10.1007/978-3-319-03542-0_8" target="_blank">https://doi.org/10.1007/978-3-319-03542-0_8</a> | |
dc.identifier.isbn | 9783319035413 | |
dc.identifier.issn | 03029743 | |
dc.identifier.uri | http://scholarbank.nus.edu.sg/handle/10635/78044 | |
dc.description.abstract | Separation logic is a state-of-the-art logic for dealing with the program heap. Using its frame rule, initial works have strived towards automated modular verification for heap-manipulating programs against user-supplied specifications. Since manually writing specifications is a tedious and error-prone engineering process, the so-called bi-abduction (a combination of the frame rule and abductive inference) is proposed to automatically infer pre/post specifications on data structure shapes. However, it has omitted the inference of pure properties of data structures such as their size, sum, height, content and minimum/maximum value, which are needed to express a higher level of program correctness. In this paper, we propose a novel approach, called pure bi-abduction, for inferring pure information for pre/post specifications, using the result from a prior shape analysis step. The power of our new bi-abductive entailment procedure is significantly enhanced by its collection of proof obligations over uninterpreted relations (functions). Additionally, we design a predicate extension mechanism to systematically extend shape predicates with pure properties. We have implemented our inference mechanism and evaluated its utility on a benchmark of programs. We show that pure properties are prerequisite to allow the correctness of about 20% of analyzed procedures to be captured and verified. © Springer International Publishing 2013. | |
dc.description.uri | http://libproxy1.nus.edu.sg/login?url=http://dx.doi.org/10.1007/978-3-319-03542-0_8 | |
dc.source | Scopus | |
dc.subject | Functional correctness | |
dc.subject | Memory safety | |
dc.subject | Program verification | |
dc.subject | Pure bi-abduction | |
dc.subject | Separation logic | |
dc.subject | Specification inference | |
dc.type | Conference Paper | |
dc.contributor.department | COMPUTER SCIENCE | |
dc.description.doi | 10.1007/978-3-319-03542-0_8 | |
dc.description.sourcetitle | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | |
dc.description.volume | 8301 LNCS | |
dc.description.page | 107-123 | |
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.