Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-319-03542-0_8
Title: Bi-abduction with pure properties for specification inference
Authors: Trinh, M.-T.
Loc, Q.
David, C.
Chin, W.-N. 
Keywords: Functional correctness
Memory safety
Program verification
Pure bi-abduction
Separation logic
Specification inference
Issue Date: 2013
Source: 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)
URI: http://scholarbank.nus.edu.sg/handle/10635/78044
ISBN: 9783319035413
ISSN: 03029743
DOI: 10.1007/978-3-319-03542-0_8
Appears in Collections:Staff Publications

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

SCOPUSTM   
Citations

5
checked on Feb 20, 2018

Page view(s)

39
checked on Feb 23, 2018

Google ScholarTM

Check

Altmetric


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