Roberto Bruni

Thanks to the locality principle, separation logics support modular, scalable analysis of large codebases by relying on local axioms and frame rules to focus only on the heap fragments required for verification. However, depending on the direction—forward vs. backward—and sense of approximation—over vs. under—of the analysis, designing the corresponding proof systems can require some ingenuity. In his work on the calculational design of program logics, Patrick Cousot outlines a methodology for deriving proof systems directly from program semantics using abstract interpretation, covering both correctness and incorrectness analyses. Unfortunately, when applied to heap-manipulating programs, Cousot’s calculational approach cannot handle the locality principle, because it does not provide a calculational way to derive frame rules and produces axioms that refer to the global heap. In this paper, we propose a general methodology for systematically deriving local axioms in which the locality principle is embedded by construction. For heap-manipulating primitives, we can derive the minimal required heap and the corresponding pre- and postconditions, complemented by universal frame rules without additional syntactic side conditions. Our method is parametric w.r.t. a set of semantic closure properties that are exploited to design local axioms; it can deal with different memory models; it favors the reuse of many inference rules across over- and under-approximation; and it produces logical systems capable of deriving a broader range of triples w.r.t. existing, cleverly designed, program logics for (in)correctness, ranging from Separation Logic (SL) and Incorrectness Separation Logic (ISL) to Separation Sufficient Incorrectness Logic (SepSIL). Furthermore, we demonstrate the flexibility of our methodology by applying it to design a novel proof system for inferring necessary preconditions with separation logic.

The verification of large codebases requires compositional analysis techniques that enable the reuse and composition of summaries previously computed for unchanged procedures or code fragments.This observation is essential for scalable program analysis and lies at the core of Separation Logic approaches.Local reasoning in Separation Logic relies on computing code summaries with minimal hypotheses about the memory locations accessed by a program fragment and then exploiting frame inference to compose specifications over larger heaps. Bi-abduction algorithms are instrumental for the automation of frame inference, as they synthesize both the missing resources required to meet a specification and the portion of memory that remains unaffected by execution.Bi-abduction was originally introduced for forward over-approximate reasoning. More recently, it has been adapted to forward under-approximate incorrectness analyses for automatic bug detection.In this paper we formalize bi-abduction within a fully general setting that is independent of both the analysis direction (forward or backward) and the sense of approximation (over or under). We first instantiate this framework to derive bi-abduction algorithms for backward analyses, encompassing both under- and over-approximate reasoning. We then propose a novel notion of full bi-abduction that is independent of both the analysis direction and the approximation discipline, yielding a single sound framework for compositional reasoning across all four combinations of forward/backward and over-/under-approximate analyses. We validate the proposed algorithms through a proof-of-concept implementation.

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.

We explore the capabilities of , a state-of-the-art toolset based on graph transformation systems, to perform different kinds of analyses of Reaction Systems, ranging from reachability and causal analysis to model checking. Our results are encouraging, as in the presence of large state spaces improves the time required for both reachability and causal analyses by an order of magnitude, compared to other available tools. From the point of view of , the implementation of Reaction Systems provided some interesting insights on the most convenient way to model certain computational requirements through negative and nested application conditions.

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.

Reaction Systems (RSs) are a qualitative model inspired by biochemical processes, where the dynamics of complex systems is modelled by a collection of local reactions. Each reaction comprises a set of reactants that triggers a set of products unless hindered by the presence of some inhibitors. The use of inhibitors introduces non-monotonic behaviours that are difficult to analyze. This work focuses on the explainability of local phenomena, like the production of certain products or the reachability of certain attractors, by separating the causes responsible for reaching them from the irrelevant elements of a possibly much larger, global statespace. The main novelty of our approach is the ability to derive sufficient conditions that combine positive dependencies (e.g., requesting the presence of some entities at a certain stage, as already done in the literature) with negative ones (e.g., requesting the absence of some entities). This is achieved by combining and extending previous “static” constructions, like the transformation to Positive RSs and the minimization of RSs with “dynamic” techniques, like the process algebraic evolution of RSs, the slicing of computation and the on-the-fly generation of negative dependencies. We compare many different combinations of the above approaches, discussing their respective benefits and trade-offs in order to identify the most convenient analysis. We demonstrate our methodology on a case study involving T cell protein interactions, showing how it can reveal critical stimulus combinations and pinpoint potential drug targets by explaining phenotype emergence. Our analysis offers new insights and greater explanatory power than existing approaches.

Reaction systems (RSs) are a computational framework inspired by the interplay between biochemical interactions. Similarly to regulatory networks, reaction products can dynamically activate or inhibit other reactions. This provides a framework for discrete-time, interactive computation, where each state is determined by those reactions enabled in the immediately preceding state and by additional environmental interventions, if any. Since their introduction, RSs have been extended to study many aspects of complex systems: multi-agent collaborations, cause-effect relationships, model checking, and many others. The gap in the literature addressed in this paper is the lack of software tools for simulating and analysing distributed reaction systems (DRSs). We introduce a process algebraic approach to describing, simulating, and analysing DRSs. This allows designing complex models by re-using modular components in a well-structured and compositional way, and analysing them with the BioReSolve modelling software. We demonstrate our approach by experimenting with distributed Lotka-Volterra models, where multiple agents evolve according to their own periodic dynamics, but can also synchronise their cycles through diverse communication topologies.