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 Award | 1 Oct 2022 |
|---|---|
| Original language | English |
| Awarding Institution |
|
| Supervisor | Shengchao Qin (Supervisor), Mengda He (Supervisor) & Chunyan Mu (Supervisor) |