Bi-Abduction for Shapes with Ordered Data

TL;DR

This paper introduces a novel one-stage bi-abductive inference procedure for combined shape and ordered data analysis, enhancing automated verification of heap-manipulating programs.

Contribution

It extends bi-abductive inference to handle both data structures and ordering values, enabling more comprehensive shape and data domain analysis.

Findings

Prototype solver demonstrates effectiveness on SL-COMP benchmarks.

Shows potential for improved specification inference in program verification.

Enhances scalability of shape analysis with ordered data integration.

Abstract

Shape analysis is of great importance for the verification of the correctness and memory-safety of heap-manipulating programs, yet such analyses have been shown to be highly difficult problems. The integration of separation logic into shape analyses has improved the effectiveness of the techniques, but the most significant advancement in this area is bi-abductive inference. Enabled by separation logic, bi-abduction - a combination of abductive inference and frame inference - is the key enabler for compositional reasoning, helping to scale up verification significantly. Indeed, the success of bi-abduction has led to the development of Infer, the tool used daily to verify Facebook's codebase of millions of lines of code. However, this success currently stays largely within the shape domain. To extend this impact towards the combination of shape and arithmetic domains, in this work, we present a novel one-stage bi-abductive procedure for a combination of data structures and ordering values. The procedure is designed in the spirit of the Unfold-and-Match paradigm where the inference is utilized to derive any mismatched portion. We have also implemented a prototype solver, based on the Cyclist library, and demonstrate its capabilities over a range of benchmarks from the SL-COMP competition. The experimental results show that our proposal shows promise for the specification inference in an automated verification of heap-manipulating programs.