An Investigation of Combined Domain Bi-Abductive Inference

Student thesis: Doctoral Thesis

Abstract

Bi-abductive inference is a well-established and eective technique for the en-
hancement of separation logic entailment provers. Capable of identifying and
correcting deciencies in an entailment through the inference of frames and anti-
frames { representing the missing and extra information from the entailment {
bi-abduction has seen a number of successful applications in verication systems.
While eective, bi-abductive inference has a number of notable limitations,
with one of the most signicant being a restriction to the inference of spatial
information only. Though uncommon, non-spatial properties may have an impact on the memory-safety properties bi-abductive techniques are typically applied to establish, making the inference of such constraints a notable improvement. Additionally, support for non-spatial properties such as ordering and contents would also open the possibility of applying bi-abductive inference to establish correctness properties of programs as well. Though a small number of bi-abductive techniques with support for the combined domain are known, these systems are dependant upon additional analysis phases, introducing overheads and potentially degrading the results produced by the system as a result. In order to more fully investigate the feasibility and potential benets such
a system could bring, a pair of novel single-step bi-abductive inference systems
operating in the combined spatial and pure domain are developed and presented: a initial system for potentially ordered singly-linked lists and trees, and a second generalised system for a more complex combined domain with user-dened predicates and support for bag, arithmetic and ordering properties. These systems were subsequently implemented as automated bi-abductive entailment provers based upon the Cyclist framework and tested over several divisions taken from the SL-COMP competition. While these implementations would not match the eectiveness of existing systems, the overall results still indicate the approach has a great deal of promise, with the implementations able to resolve the majority of examples in modest times with reasonable inferred corrections, where needed.
Date of Award1 Oct 2022
Original languageEnglish
Awarding Institution
  • Teesside University
SupervisorShengchao Qin (Supervisor), Mengda He (Supervisor) & Chunyan Mu (Supervisor)

Cite this

'