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 combining correctness and incorrectness 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 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 legitimizes heuristics that avoid exhaustive path enumeration (e.g., selective disjunct pruning, loop unrolling). Concretely, we instrument the proof rules of the second logic with derivations 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 scalable, expressive, automated code contracts.

Sound over-approximation methods are effective for proving the absence of errors, but inevitably produce false alarms that can hamper programmers. In contrast, under-approximation methods focus on bug detection and are free from false alarms. In this work, we present two novel proof systems designed to locate the source of errors via backward under-approximation, namely Sufficient Incorrectness Logic (SIL) and its specialization for handling memory errors, called Separation SIL. The SIL proof system is minimal, sound and complete for Lisbon triples, enabling a detailed comparison of triple-based program logics across various dimensions, including negation, approximation, execution order, and analysis objectives. More importantly, SIL lays the foundation for our main technical contribution, by distilling the inference rules of Separation SIL, a sound and (relatively) complete proof system for automated backward reasoning in programs involving pointers and dynamic memory allocation. The completeness result for Separation SIL relies on a careful crafting of both the assertion language and the rules for atomic commands.

Local Completeness Logic (LCL) is a proof system for program analysis rooted in abstract interpretation. The program semantics is under-approximated by any provable postcondition, like incorrectness logic does, but it is also over-approximated by a (locally) complete abstraction of such a postcondition, like Hoare logic does. Therefore, any derivable triple will either prove the program to be correct or unveil true bugs. While the completeness of a program's function with respect to an abstract domain is inherently extensional , LCL's rules demand the preservation of local completeness throughout the abstract interpreter's computations. This characteristic renders LCL analysis intensional , meaning it depends on the way the program is written. Consequently, LCL proof system may not derive all the valid triples. This paper addresses this discrepancy by: 1) designing new rules that allow one to perform part of the intensional analysis in different (complete) abstract domains whenever necessary; and 2) to compare their expressiveness. Notably, some of these new rules enable the derivation of all extensionally valid triples, thereby decoupling the set of provable properties from the way the program is written.

The main goal of most static analyses is to prove the absence of bugs : if the analysis reports no alarms, then the program will not exhibit any unwanted behaviours. For this reason, they are designed to over-approximate program behaviours and, consequently, they can report some false alarms. O’Hearn’s recent work on incorrectness has renewed the interest in the use of under-approximations for bug finding , because they only report true alarms. In principle, Abstract Interpretation techniques can handle under-approximations as well as over-approximations, but, in practice, few attempts were developed for the former, notwithstanding the much wider literature on the latter. In this article, we investigate the possibility of exploiting under-approximation abstract domains for bug-finding analyses. First we restrict to consider concrete powerset domains and highlight some intuitive asymmetries between over- and under-approximations. Then, we prove that the effectiveness of abstract domains defined by under-approximation Galois connection is limited because the analysis is likely to return trivial results whenever common transfer functions are encoded in the program. To this aim, we introduce the original concepts of non-emptying functions and highly surjective function family , and we prove the nonexistence of abstract domains able to under-approximate such functions in a non-trivial way. We show many examples of finite and infinite numerical domains, as well as other generic domains. In all such cases, we prove the impossibility of performing non-trivial analyses via under-approximation Galois connections.

Abstract We formulate, in lattice-theoretic terms, two novel algorithms inspired by Bradley’s property directed reachability algorithm. For finding safe invariants or counterexamples, the first algorithm exploits over-approximations of both forward and backward transition relations, expressed abstractly by the notion of adjoints. In the absence of adjoints, one can use the second algorithm, which exploits lower sets and their principals. As a notable example of application, we consider quantitative reachability problems for Markov Decision Processes.

Abstract Abstract interpretation is a framework to design sound static analyses by over-approximating the set of program behaviours. While over-approximations can prove correctness, they cannot witness incorrectness because false alarms may arise. An ideal, but uncommon, situation is completeness of the abstraction that can ensure no false alarm is introduced by the abstract interpreter. Local Completeness Logic is a proof system that can decide both correctness and incorrectness of a program: any provable triple $$\vdash _{A}[P]~\textsf{c}~[Q]$$ ⊢ A [ P ] c [ Q ] in the logic implies completeness of an intensional abstraction of program $$\textsf{c}$$ c on input P and is such that Q can be used to decide (in)correctness. However, completeness itself is an extensional property of the function computed by the program, while the above intensional analysis depends on the way the program is written and therefore not all valid triples can be derived in the proof system. Our main contribution is the study of new inference rules which allow one to perform part of the intensional analysis in a more precise abstract domain, and then to transfer the result back to the coarser domain. With these new rules, all (extensionally) valid triples can be derived in the proof system, thus untying the set of provable properties from the way the program is written.

Abstract Static analyses are mostly designed to show the absence of bugs: if the analysis reports no alarms then the program won’t exhibit any unwanted behaviours. To this aim they manipulate over-approximations of program semantics and, inevitably, they often report some false alarms. Recently, O’Hearn proposed Incorrectness Logic, that is based on under-approximations, as a formal method to find bugs that only reports true alarms. In this paper we aim to answer one important question raised by O’Hearn, namely which role can Abstract Interpretation play for the development of under-approximate tools for bug catching. In principle, Abstract Interpretation based static analyses can be defined for computing over-approximations as well as under-approximations, but in practice, most techniques exploited the former while few attempts developed the latter. To show why it is difficult to design effective under-approximation abstract domains, we first propose the new definitions of non emptying functions and highly surjective function family and then we formally prove the limits of under-approximation analysis by showing the non existence of abstract domains able to approximate such functions in a non trivial way. Our results outline the limits of under-approximation Abstract Interpretation and clarify, for the first time, why over- and under- approximation analyzers exhibited such a different development.