Bi-Abduction with Pure Properties for Specification Inference

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.