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.

Abstract 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.

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.

Abstract This paper forges a strong connection between two well known computational frameworks for representing biological systems, in order to facilitate the seamless transfer of techniques between them. Boolean networks are a well established formalism employed from biologists. They have been studied under different (synchronous and asynchronous) update semantics, enabling the observation and characterisation of distinct facets of system behaviour. Recently, a new semantics for Boolean networks has been proposed, called most permissive semantics, that enables a more faithful representation of biological phenomena. Reaction systems offer a streamlined formalism inspired by biochemical reactions in living cells. Reaction systems support a full range of analysis techniques that can help for gaining deeper insights into the underlying biological phenomena. Our goal is to leverage the available toolkit for predicting and comprehending the behaviour of reaction systems within the realm of Boolean networks. In this paper, we first extend the behaviour of reaction systems to several asynchronous semantics, including the most permissive one, and then we demonstrate that Boolean networks and reaction systems exhibit isomorphic behaviours under the synchronous, general/fully asynchronous and most permissive semantics.

Abstract Cause/effect analysis of complex systems is instrumental in better understanding many natural phenomena. Moreover, formal analysis requires the availability of suitable abstract computational models that somehow preserve the features of interest. Our contribution focuses on the analysis of Reaction Systems (RSs), a qualitative computational formalism inspired by biochemical reactions in living cells. The primary challenge lies in dealing with inhibition mechanisms. On the one hand, inhibitors enhance the expressiveness of the computational abstraction; on the other hand, they can introduce nonmonotonic behaviors that can be computationally hard to deal with in the analysis. We propose an encoding of RSs into an equivalent formulation without inhibitors (called Positive RSs, PRSs for short) that is easier to handle, because PRSs exhibit monotonic behaviors. The effectiveness of our transformation is witnessed by its impact on two different techniques for cause/effect analysis. The first, called slicing, allows detecting the causes of some unforeseen phenomenon by reasoning backward along a given computation. Here, PRSs can be exploited to improve the quality of the analysis. The second technique, predictor analysis, is addressed by introducing a novel tool called MuMa, which is based on must/maybe sets, whence the tool name, an original abstraction for approximating ancestor formulas. MuMa exploits PRSs to improve the performance of the analysis.

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 interpretation is a well-known and extensively used method to extract over-approximate program invariants by a sound program analysis algorithm. Soundness means that no program errors are lost and it is, in principle, guaranteed by construction. Completeness means that the abstract interpreter reports no false alarms for all possible inputs, but this is extremely rare because it needs a very precise analysis. We introduce a weaker notion of completeness, called local completeness , which requires that no false alarms are produced only relatively to some fixed program inputs. Based on this idea, we introduce a program logic, called Local Completeness Logic for an abstract domain A , for proving both the correctness and incorrectness of program specifications. Our proof system, which is parameterized by an abstract domain A , combines over- and under-approximating reasoning. In a provable triple ⊦ A [ p ] 𝖼 [ q ], 𝖼 is a program, q is an under-approximation of the strongest post-condition of 𝖼 on input p such that their abstractions in A coincide. This means that q is never too coarse, namely, under some mild assumptions, the abstract interpretation of 𝖼 does not yield false alarms for the input p iff q has no alarm . Therefore, proving ⊦ A [ p ] 𝖼 [ q ] not only ensures that all the alarms raised in q are true ones, but also that if q does not raise alarms, then 𝖼 is correct. We also prove that if A is the straightforward abstraction making all program properties equivalent, then our program logic coincides with O’Hearn’s incorrectness logic, while for any other abstraction, contrary to the case of incorrectness logic, our logic can also establish program correctness.

Abstract Reaction systems (RSs) are a successful natural computing framework inspired by chemical reaction networks. A RS consists of a set of entities and a set of reactions. Entities can enable or inhibit each reaction and are produced by reactions or provided by the environment. In this paper, we define two quantitative variants of RSs: the first one is along the time dimension, to specify delays for making available reactions products and durations to protract their permanency, while the second deals with the possibility to specify different concentration levels of a substance in order to enable or inhibit a reaction. Technically, both extensions are obtained by modifying in a modular way the Structural Operational Semantics (SOS) for RSs that was already defined in the literature. Our approach maintains several advantages of the original semantics definition that were: (1) providing a formal specification of the RS dynamics that enables the reuse of many formal analysis techniques and favours the implementation of tools, and (2) making the RS framework extensible, by adding or changing some of the SOS rules in a compositional way. We provide a prototype logic programming implementation and apply our tool to three different case studies: the tumour growth, the Th cell differentiation in the immune system and neural communication.

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.

Abstract interpretation is a sound-by-construction method for program verification: any erroneous program will raise some alarm. However, the verification of correct programs may yield false-alarms, namely it may be incomplete. Ideally, one would like to perform the analysis on the most abstract domain that is precise enough to avoid false-alarms. We show how to exploit a weaker notion of completeness, called local completeness, to optimally refine abstract domains and thus enhance the precision of program verification. Our main result establishes necessary and sufficient conditions for the existence of an optimal, locally complete refinement, called pointed shell. On top of this, we define two repair strategies to remove all false-alarms along a given abstract computation: the first proceeds forward, along with the concrete computation, while the second moves backward within the abstract computation. Our results pave the way for a novel modus operandi for automating program verification that we call Abstract Interpretation Repair (AIR): instead of choosing beforehand the right abstract domain, we can start in any abstract domain and progressively repair its local incompleteness as needed. In this regard, AIR is for abstract interpretation what CEGAR is for abstract model checking.

We introduce the notion of local completeness in abstract interpretation and define a logic for proving both the correctness and incorrectness of some program specification. Abstract interpretation is extensively used to design sound-by-construction program analyses that over-approximate program behaviours. Completeness of an abstract interpretation A for all possible programs and inputs would be an ideal situation for verifying correctness specifications, because the analysis can be done compositionally and no false alert will arise. Our first result shows that the class of programs whose abstract analysis on A is complete for all inputs has a severely limited expressiveness. A novel notion of local completeness weakens the above requirements by considering only some specific, rather than all, program inputs and thus finds wider applicability. In fact, our main contribution is the design of a proof system, parameterized by an abstraction A, that, for the first time, combines over- and under-approximations of program behaviours. Thanks to local completeness, in a provable triple ⊢A [P ] c [Q], the assertion Q is an under-approximation of the strongest post-condition post[c](P ) such that the abstractions in A of Q and post[c](P ) coincide. This means that Q is never too coarse, namely, under mild assumptions, the abstract interpretation of c does not yield false alerts for the input P iff Q has no alert. Thus, ⊢ A [P ] c [Q] not only ensures that all the alerts raised in Q are true ones, but also that if Q does not raise alerts then c is correct.

Gene regulatory networks represent the interactions among genes regulating the activation of specific cell functionalities and they have been successfully modeled using threshold Boolean networks. In this paper we propose a systematic translation of threshold Boolean networks into reaction systems. Our translation produces a non redundant set of rules with a minimal number of objects. This translation allows us to simulate the behavior of a Boolean network simply by executing the (closed) reaction system we obtain. This can be very useful for investigating the role of different genes simply by “playing” with the rules. We developed a tool able to systematically translate a threshold Boolean network into a reaction system. We use our tool to translate two well known Boolean networks modelling biological systems: the yeast-cell cycle and the SOS response in Escherichia coli. The resulting reaction systems can be used for investigating dynamic causalities among genes.

Abstract In reaction systems, preimages and nth ancestors are sets of reactants leading to the production of a target set of products in either 1 or n steps, respectively. Many computational problems on preimages and ancestors, such as finding all minimum-cardinality nth ancestors, computing their size or counting them, are intractable. In this paper, we characterize all nth ancestors using a Boolean formula that can be computed in polynomial time. Once simplified, this formula can be exploited to easily solve all preimage and ancestor problems. This allows us to directly relate the difficulty of ancestor problems to the cost of the simplification so that new insights into computational complexity investigations can be achieved. In particular, we focus on two problems: (i) deciding whether a preimage/nth ancestor exists and (ii) finding a preimage/nth ancestor of minimal size. Our approach is constructive, it aims at finding classes of reactions systems for which the ancestor problems can be solved in polynomial time, in exact or approximate way.

Verification of C/C++ programs has seen considerable progress in several areas, but not for programs that use these languages’ mathematical libraries. The reason is that all libraries in widespread use come with no guarantees about the computed results. This would seem to prevent any attempt at formal verification of programs that use them: without a specification for the functions, no conclusion can be drawn statically about the behavior of the program. We propose an alternative to surrender. We introduce a pragmatic approach that leverages the fact that most math.h/cmath functions are almost piecewise monotonic: as we discovered through exhaustive testing, they may have glitches , often of very small size and in small numbers. We develop interval refinement techniques for such functions based on a modified dichotomic search, which enable verification via symbolic execution based model checking, abstract interpretation, and test data generation. To the best of our knowledge, our refinement algorithms are the first in the literature to be able to handle non-correctly rounded function implementations, enabling verification in the presence of the most common implementations. We experimentally evaluate our approach on real-world code, showing its ability to detect or rule out anomalous behaviors.

In this paper we generalise the notion of extensional (functional) equivalence of programs to abstract equivalences induced by abstract interpretations . The standard notion of extensional equivalence is recovered as the special case, induced by the concrete interpretation. Some properties of the extensional equivalence, such as the one spelled out in Rice’s theorem, lift to the abstract equivalences in suitably generalised forms. On the other hand, the generalised framework gives rise to interesting and important new properties, and allows refined, non-extensional analyses. In particular, since programs turn out to be extensionally equivalent if and only if they are equivalent just for the concrete interpretation, it follows that any non-trivial abstract interpretation uncovers some intensional aspect of programs. This striking result is also effective, in the sense that it allows constructing, for any non-trivial abstraction, a pair of programs that are extensionally equivalent, but have different abstract semantics. The construction is based on the fact that abstract interpretations are always sound, but that they can be made incomplete through suitable code transformations. To construct these transformations, we introduce a novel technique for building incompleteness cliques of extensionally equivalent yet abstractly distinguishable programs: They are built together with abstract interpretations that produce false alarms. While programs are forced into incompleteness cliques using both control-flow and data-flow transformations, the main result follows from limitations of data-flow transformations with respect to control-flow ones. A further consequence is that the class of incomplete programs for a non-trivial abstraction is Turing complete. The obtained results also shed a new light on the relation between the techniques of code obfuscation and the precision in program analysis.

Reaction systems are a qualitative formalism for modeling systems of biochemical reactions. They describe the evolution of sets of objects representing biochemical molecules. One of the main characteristics of Reaction systems is the non-permanency of the objects, namely objects disappear if not pr oduced by any enabled reaction. Reaction systems execute in an environment that provides new objects at each step. Causality properties of reaction systems can be studied by using notions of formula based predictor. In this context, we define a notion of opacity that can be used to study information flow properties for reaction systems. Objects will be partitioned into high level (invisible) and low level (visible) ones. Opacity ensures that the presence (or absence) of high level objects cannot be guessed observing the low level objects only. Such a property is shown to be decidable and computable by exploiting the algorithms for minimal formula based predictors.

Abstract Code protection technologies require anti reverse engineering transformations to obfuscate programs in such a way that tools and methods for program analysis become ineffective. We introduce the concept of model deformation inducing an effective code obfuscation against attacks performed by abstract model checking. This means complicating the model in such a way a high number of spurious traces are generated in any formal verification of the property to disclose about the system under attack.We transform the program model in order to make the removal of spurious counterexamples by abstraction refinement maximally inefficient. Because our approach is intended to defeat the fundamental abstraction refinement strategy, we are independent from the specific attack carried out by abstract model checking. A measure of the quality of the obfuscation obtained by model deformation is given together with a corresponding best obfuscation strategy for abstract model checking based on partition refinement.

Reaction systems are a qualitative formalism for modeling systems of biochemical reactions characterized by the non-permanency of the elements: molecules disappear if not produced by any enabled reaction. Reaction systems execute in an environment that provides new molecules at each step. Brijder, Ehrenfeucht and Rozemberg introduced the idea of predictors. A predictor of a molecule s, for a given n, is the set of molecules to be observed in the environment to determine whether s is produced or not at step n by the system. We introduced the notion of formula based predictor, that is a propositional logic formula that precisely characterizes environments that lead to the production of s after n steps. In this paper we revise the notion of formula based predictor by defining a specialized version that assumes the environment to provide molecules according to what expressed by a temporal logic formula. As an application, we use specialized formula based predictors to give theoretical grounds to previously obtained results on a model of gene regulation.

Floating-point computations are quickly finding their way in the design of safety- and mission-critical systems, despite the fact that designing floating-point algorithms is significantly more difficult than designing integer algorithms. For this reason, verification and validation of floating-point computations are hot research topics. An important verification technique, especially in some industrial sectors, is testing. However, generating test data for floating-point intensive programs proved to be a challenging problem. Existing approaches usually resort to random or search-based test data generation, but without symbolic reasoning it is almost impossible to generate test inputs that execute complex paths controlled by floating-point computations. Moreover, because constraint solvers over the reals or the rationals do not natively support the handling of rounding errors, the need arises for efficient constraint solvers over floating-point domains. In this paper, we present and fully justify improved algorithms for the propagation of arithmetic IEEE 754 binary floating-point constraints. The key point of these algorithms is a generalization of an idea by B. Marre and C. Michel that exploits a property of the representation of floating-point numbers.

Verifying critical numerical software involves the generation of test data for floating-point intensive programs. As the symbolic execution of floating-point computations presents significant difficulties, existing approaches usually resort to random or search-based test data generation. However, without symbolic reasoning, it is almost impossible to generate test inputs that execute many paths with floating-point computations. Moreover, constraint solvers over the reals or the rationals do not handle the rounding errors. In this paper, we present a new version of FPSE, a symbolic evaluator for C program paths, that specifically addresses this problem. The tool solves path conditions containing floating-point computations by using correct and precise projection functions. This version of the tool exploits an essential filtering property based on the representation of floating-point numbers that makes it suitable to generate path-oriented test inputs for complex paths characterized by floating-point intensive computations. The paper reviews the key implementation choices in FPSE and the labeling search heuristics we selected to maximize the benefits of enhanced filtering. Our experimental results show that FPSE can generate correct test inputs for selected paths containing several hundreds of iterations and thousands of executable floating-point statements on a standard machine: this is currently outside the scope of any other symbolic-execution test data generator tool.

We study some properties of SLD-trees related to nite failure. The main results are a theorem stating that the non-ground nite failure set is a correct and fully abstract semantics wrt nite failure and a second theorem stating that the complement of non ground nite failure is andcompositional, i.e. that the nite failure behaviour of conjunctive goals can be derived from the nite failure behaviour of atomic goals. The proofs are based on two new lemmata which generalize to innite derivations theorems which are valid for successful and nitely failed derivations. 1 Introduction The operational semantics of (positive) logic programs is usually based on SLDtrees. Several operational properties, useful for reasoning about programs, can be extracted from an SLD-tree. Examples are SLD-derivations, resultants, partial answers, computed answers, nite failures. All these properties, that we call observables, can be obtained as abstractions of the SLD-tree. The study of the obser...