Please use this identifier to cite or link to this item:
|Title:||Bi-abduction with pure properties for specification inference|
|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. https://doi.org/10.1007/978-3-319-03542-0_8|
|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.|
|Source Title:||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Oct 14, 2018
checked on Aug 10, 2018
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.