U-Turn: Enhancing Incorrectness Analysis by Reversing Direction
Flavio Ascari, Roberto Bruni, Roberta Gori, Azalea Raad
TL;DR
The paper addresses the adoption gap in formal verification by combining Incorrectness Logic (IL) with Sufficient Incorrectness Logic (SIL) through a novel U-Turn framework. By reusing IL-derived path information to guide the subsequent SIL backward analysis, it achieves more informative analyses that expose both reachable errors and their causes. It introduces a sound and complete axiom-schema for atomic commands to derive IL/SIL triples and articulates a two-pass strategy in which IL analysis followed by SIL backward reasoning is orchestrated by explicit U-Turn rules. The work also relates the approach to UNTer, demonstrates the method on representative examples, and outlines future work on completeness, heap-locality extensions, and integration with abstraction techniques. Overall, U-Turn provides a principled, automated way to fuse forward and backward incorrectness reasoning to produce precise, practically actionable code contracts and debugging insights.
Abstract
O'Hearn's Incorrectness Logic (IL) has sparked renewed interest in static analyses that aim to detect program errors rather than prove their absence, thereby avoiding false alarms -- a critical factor for practical adoption in industrial settings. As new incorrectness logics emerge to capture diverse error-related properties, a key question arises: can the combination of (in)correctness techniques enhance precision, expressiveness, automation, or scalability? Notable frameworks, such as outcome logic, UNTer, local completeness logic, and exact separation logic, unify multiple analyses within a single proof system. In this work, we adopt a complementary strategy. Rather than designing a unified logic, we combine IL, which identifies reachable error states, with Sufficient Incorrectness Logic (SIL), which finds input states potentially leading to those errors. As a result, we get a more informative and effective analysis than either logic in isolation. Rather than naively sequencing them, our key innovation is reusing heuristic choices from the first analysis to steer the second. In fact, both IL and SIL rely on under-approximation and thus their automation legitimates heuristics that avoid exhaustive path enumeration (e.g., selective disjunct pruning, loop unrolling). Concretely, we instrument the second logic's proof rules with derivations coming from the first to inductively guide rule selection and application. To our knowledge, this is the first rule format enabling such inter-analysis instrumentation. This combined analysis aids debugging and testing by revealing both reachable errors and their causes, and opens new avenues for embedding incorrectness insights into (a new kind of) scalable, expressive, automated code contracts.