Bi-Abduction in Separation Logic with Arrays and Lists for Program Analysis

This paper gives an algorithm that solves the bi-abduction problem in symbolic-heap separation logic with arrays and lists. The logic is an assertion language of Hoare-style logic for program verification of pointer manipulating programs. The bi-abduction problem asks to find an additional assumption and an additional conclusion from a given assumption and a given conclusion such that the entailment becomes true. Bi-Abduction is indispensable for modular analysis and automatic verification with separation logic, since the condition at a call site that calls a function and the precondition of the called function are analyzed separately by modular analysis, and they both may contain spatial formulas of separation logic, and we have to guarantee they become the same by adding some spartial formulas to each of them. This paper shows the correctness of the bi-abduction algorithm with detailed proofs. A bi-abduction solver based on the algorithm has been implemented as a part of the authors’ automatic program verifier, and experimental results of the bi-abduction solver with small inputs are also shown, which show the algorithm is usable. © 2024 Japan Society for Software Science and Technology. All rights reserved.