Separation Logic (SL) is a well-established framework for reasoning about programs that manipulate dynamic memory. To express and verify properties of custom recursive data structures, SL is extended with spatial predicates defined by user-specified inductive rules. Many verification problems reduce to deciding entailments between formulas involving these predicates. While the general entailment problem is undecidable, a broad class of inductive rules - known as PCE (Progressing, Connected, and Established) - has been identified for which entailment is decidable. In this work, we extend the study of the entailment problem to Dynamic Separation Logic (DSL), an extension of SL that includes dynamic modalities for reasoning about actions on the heap and store. We show that entailment in DSL remains decidable for PCE rules by proving that dynamic modalities can be automatically eliminated.

Abstract This paper presents a novel extension of the superposition calculus for reasoning about formulas in Separation Logic (SL). Our approach integrates the efficiency of saturation-based theorem proving with the expressive power of SL, which is widely used to describe and reason about memory heaps. The target logic strictly extends first-order equational logic with SL constructs built from points-to atoms and separating conjunctions. The resulting calculus retains the core strengths of the superposition paradigm while addressing the distinctive semantic challenges of SL. We prove that the calculus is sound and complete w.r.t the standard redundancy criterion.

Separation Logic (SL) enables reasoning about programs that manipulate pointers. Its key feature is the separating conjunction ⋆, which asserts that two formulas hold on disjoint portions of memory. We consider an extension of SL, called Overlaid SL (OSL), that allows non-disjoint combinations of data structures defined over different fields, enriched with set constraints on the nodes of these structures. We prove that entailment is decidable for a broad class of data structures satisfying the so-called PCE conditions of [Iosif et al., 2013], thus extending this result to OSL. Our decision procedure is nondeterministic with doubly exponential time complexity.

We revisit a longstanding question about the shortest single axioms for positive implicational logic. Meredith discovered several 17-symbol single axioms and asked whether shorter ones exist. Later work reduced the problem to four candidate formulas of length 15. Using the automated theorem prover Vampire, we compute saturated clause sets that yield counter models showing that three of these candidates are not single axioms. This demonstrates the effectiveness of saturation-based reasoning for such problems, which have traditionally been studied via finite model searches.

We establish various complexity results for the entailment problem between formulas in Separation Logic with user-defined predicates denoting recursive data structures. The considered fragments are characterized by syntactic conditions on the inductive rules that define the semantics of the predicates. We focus on so-called P-rules, which are similar to (but simpler than) the PCE rules introduced by Iosif et al. in 2013. In particular, for a specific fragment where predicates are defined by so-called loc-deterministic inductive rules, we devise a sound and complete cyclic proof procedure running in polynomial time. Several complexity lower bounds are provided, showing that any relaxing of the provided conditions makes the problem intractable.

Abstract The predicate definitions in Separation Logic (SL) play an important role: they capture a large spectrum of unbounded heap shapes due to their inductiveness. This expressiveness power comes with a limitation: the entailment problem is undecidable if predicates have general inductive definitions (ID). Iosif et al. [8] proposed syntactic and semantic conditions, called PCE, on the ID of predicates to ensure the decidability of the entailment problem. We provide a (possibly nonterminating) algorithm to transform arbitrary ID into equivalent PCE definitions when possible. We show that the existence of an equivalent PCE definition for a given ID is undecidable, but we identify necessary conditions that are decidable. The algorithm has been implemented, and experimental results are reported on a benchmark, including significant examples from .

Abstract Some techniques are proposed for reasoning on co-inductive structures. First, we devise a sound axiomatization of (conservative extensions) of such structures, thus reducing the problem of checking whether a formula admits a co-inductive model to a first-order satisfiability test. We devise a class of structures, called regularly co-inductive, for which the axiomatization is complete (for other co-inductive structures, the proposed axiomatization is sound, but not complete). Then, we propose proof calculi for reasoning on such structures. We first show that some of the axioms mentioned above can be omitted if the inference rules are able to handle rational terms. Furthermore, under some conditions, some other axioms may be replaced by an additional inference rule that computes the solutions of fixpoint equations. Finally, we show that a stronger completeness result can be established under some additional conditions on the signature.

Abstract We propose a superposition-based proof procedure to reason on equational first order formulas defined over graphs. First, we introduce the considered graphs that are directed labeled graphs with lists of roots standing for pins or interfaces for replacements. Then the syntax and semantics of the considered logic are defined. The formulas at hand are clause sets built on equations and disequations on graphs. Afterwards, a sound and complete proof procedure is provided, and redundancy criteria are introduced to dismiss useless clauses and improve the efficiency of the procedure. In a first step, a set of inferences rules is provided in the case of uninterpreted labels. In a second step, the proposed rules are lifted to take into account labels defined as terms interpreted in some arbitrary theory. Particular formulas of interest are Horn clauses, for which stronger redundancy criteria can be devised. Essential differences with the usual term superposition calculus are emphasized.

Abstract We investigate the satisfiability problem for a fragment of Separation Logic (SL) with inductively defined spatial predicates and permissions. We show that the problem is undecidable in general, but decidable under some restrictions on the rules defining the semantics of the spatial predicates. Furthermore, if the satisfiability of permission formulas can be tested in exponential time for the considered permission model then SL satisfiability isExptimecomplete.

Building on previous results concerning the decidability of the satisfiability and entailment problems for separation logic formulas with inductively defined predicates, we devise a proof procedure to reason on dynamic transformations of memory heaps. The initial state of the system is described by a separation logic formula of some particular form, its evolution is modeled by a finite transition system and the expected property is given as a linear temporal logic formula built over assertions in separation logic.

Abstract The entailment problem $$\upvarphi \models \uppsi $$ φ⊧ψ in Separation Logic [12, 15], between separated conjunctions of equational ( $$x \approx y$$ x≈y and $$x \not \approx y$$ x≉y ), spatial ( $$x \mapsto (y_1,\ldots ,y_\upkappa )$$ x↦(y1,…,yκ) ) and predicate ( $$p(x_1,\ldots ,x_n)$$ p(x1,…,xn) ) atoms, interpreted by a finite set of inductive rules, is undecidable in general. Certain restrictions on the set of inductive definitions lead to decidable classes of entailment problems. Currently, there are two such decidable classes, based on two restrictions, calledestablishment[10, 13, 14] andrestrictedness[8], respectively. Both classes are shown to be in $$\mathsf {2\text {EXPTIME}}$$ 2EXPTIME by the independent proofs from [14] and [8], respectively, and a many-one reduction of established to restricted entailment problems has been given [8]. In this paper, we strictly generalize the restricted class, by distinguishing the conditions that apply only to the left- ( $$\upvarphi $$ φ ) and the right- ( $$\uppsi $$ ψ ) hand side of entailments, respectively. We provide a many-one reduction of this generalized class, calledsafe, to the established class. Together with the reduction of established to restricted entailment problems, this new reduction closes the loop and shows that the three classes of entailment problems (respectively established, restricted and safe) form a single, unified, $$\mathsf {2\text {EXPTIME}}$$ 2EXPTIME -complete class.

We define a class of Separation Logic formulae, whose entailment problem: given formulae $ϕ, ψ_1, \ldots, ψ_n$, is every model of $ϕ$ a model of some $ψ_i$? is 2EXPTIME-complete. The formulae in this class are existentially quantified separating conjunctions involving predicate atoms, interpreted by the least sets of store-heap structures that satisfy a set of inductive rules, which is also part of the input to the entailment problem. Previous work consider established sets of rules, meaning that every existentially quantified variable in a rule must eventually be bound to an allocated location, i.e. from the domain of the heap. In particular, this guarantees that each structure has treewidth bounded by the size of the largest rule in the set. In contrast, here we show that establishment, although sufficient for decidability (alongside two other natural conditions), is not necessary, by providing a condition, called equational restrictedness, which applies syntactically to (dis-)equalities. The entailment problem is more general in this case, because equationally restricted rules define richer classes of structures, of unbounded treewidth. In this paper we show that (1) every established set of rules can be converted into an equationally restricted one and (2) the entailment problem is 2EXPTIME-complete in the latter case, thus matching the complexity of entailments for established sets of rules.

We introduce a class of rooted graphs which are expressive enough to encode various kinds of classical or quantum circuits. We then follow a set-theoretic approach to define rewrite systems over the considered graphs. Afterwards, we tackle the problem of equational reasoning with the graphs under study and we propose a new Superposition calculus to check the unsatisfiability of formulas consisting of equations or disequations over these graphs. We establish the soundness and refutational completeness of the calculus.

The entailment between separation logic formulæ with inductive predicates, also known as sym- bolic heaps, has been shown to be decidable for a large class of inductive definitions [7]. Recently, a 2-EXPTIME algorithm was proposed [10, 14] and an EXPTIME-hard bound was established in [8]; however no precise lower bound is known. In this paper, we show that deciding entailment between predicate atoms is 2-EXPTIME-hard. The proof is based on a reduction from the membership problem for exponential-space bounded alternating Turing machines [5].

This article investigates the satisfiability problem for Separation Logic with k record fields, with unrestricted nesting of separating conjunctions and implications. It focuses on prenex formulæ with a quantifier prefix in the language ∃*∀* that contain uninterpreted (heap-independent) predicate symbols. In analogy with first-order logic, we call this fragment Bernays-Schönfinkel-Ramsey Separation Logic [BSR(SL k )]. In contrast with existing work on Separation Logic, in which the universe of possible locations is assumed to be infinite, we consider both finite and infinite universes in the present article. We show that, unlike in first-order logic, the (in)finite satisfiability problem is undecidable for BSR(SL k ). Then we define two non-trivial subsets thereof, for which the finite and infinite satisfiability problems are PSPACE-complete, respectively, assuming that the maximum arity of the uninterpreted predicate symbols does not depend on the input. These fragments are defined by controlling the polarity of the occurrences of separating implications, as well as the occurrences of universally quantified variables within their scope. These decidability results have natural applications in program verification, as they allow to automatically prove lemmas that occur in, e.g., entailment checking between inductively defined predicates and validity checking of Hoare triples expressing partial correctness conditions.

Abstract This paper investigates the satisfiability problem for Separation Logic with k record fields, with unrestricted nesting of separating conjunctions and implications, for prenex formulæ with quantifier prefix $$\exists ^*\forall ^*$$ . In analogy with first-order logic, we call this fragment Bernays-Schönfinkel-Ramsey Separation Logic [ $$\mathsf {BSR}(\mathsf {SL}^{\!\scriptstyle {k}})$$ ]. In contrast to existing work in Separation Logic, in which the universe of possible locations is assumed to be infinite, both finite and infinite universes are considered. We show that, unlike in first-order logic, the (in)finite satisfiability problem is undecidable for $$\mathsf {BSR}(\mathsf {SL}^{\!\scriptstyle {k}})$$ . Then we define two non-trivial subsets thereof, that are decidable for finite and infinite satisfiability respectively, by controlling the occurrences of universally quantified variables within the scope of separating implications, as well as the polarity of the occurrences of the latter. Beside the theoretical interest, our work has natural applications in program verification, for checking that constraints on the shape of a data-structure are preserved by a sequence of transformations.

A procedure is proposed to efficiently generate sets of ground implicates of first-order formulas with equality. It is based on a tuning of the superposition calculus, enriched with rules that add new hypotheses on demand during the proof search. Experimental results are presented, showing that the proposed approach is more efficient than state-of-the-art systems.

We present an algorithm for the generation of prime implicates in equational logic, that is, of the most general consequences of formulæ containing equations and disequations between first-order terms. This algorithm is defined by a calculus that is proved to be correct and complete. We then focus on the case where the considered clause set is ground, i.e., contains no variables, and devise a specialized tree data structure that is designed to efficiently detect and delete redundant implicates. The corresponding algorithms are presented along with their termination and correctness proofs. Finally, an experimental evaluation of this prime implicate generation method is conducted in the ground case, including a comparison with state-of-the-art propositional and first-order prime implicate generation tools.

International audience

International audience

Modern SoCs are characterized by increasing power density and consequently increasing temperature, that directly impacts performances, reliability and cost of a device through its packaging. Thermal issues need to be predicted and mitigated as early as possible in the design flow, when the optimization opportunities are the highest. In this paper, we present an efficient framework for the design of dynamic thermal mitigation schemes based on a high-level SystemC virtual prototype tightly coupled with efficient power and thermal simulation tools. We demonstrate the benefit of our approach through silicon comparison with the SThorm 64-core architecture and provide simulation speed results making it a sound solution for the design of thermal mitigation early in the flow.

To offer more computing power to modern SoCs, transistors keep scaling in new technology nodes. Consequently, the power density is increasing, leading to higher thermal risks. Thermal issues need to be addressed as early as possible in the design flow, when the optimization opportunities are the highest. For early design stages, architects rely on virtual prototypes to model their designs' behavior with an adapted trade-off between accuracy and simulation speed. Unfortunately, accurate virtual prototypes fail to encompass thermal effects timescale. In this paper, we demonstrate that less accurate high-level architectural models, in conjunction with efficient power and thermal simulation tools, provide an adapted environment to analyze thermal issues and design software thermal mitigation solutions in the case of the Locomotiv MPSoC architecture.

We study the complexity of the satisfiability problem for a class of logical formulae called iterated propositional schemata, modelling infinite sequences of structurally similar propositional formulae (such as the sequence where n ∊ ℕ). We prove that the problem is EXPSPACE-complete in general and PSPACE-complete if the numbers occurring in the formula are polynomially bounded by the size of the schema. We then consider more restricted classes: we prove that the problem is still PSPACE-complete for the Horn class, but only NP-complete for the Krom class (sets of clauses of length 2). Finally, we devise a simple criterion ensuring that the satisfiability problem is in P.

We devise a resolution calculus that tests the satisfiability of infinite families of clause sets, called clause set schemata. For schemata of propositional clause sets, we prove that this calculus is sound, refutationally complete, and terminating. The calculus is extended to first-order clauses, for which termination is lost, since the satisfiability problem is not semi-decidable for nonpropositional schemata. The expressive power of the considered logic is strictly greater than the one considered in our previous work.

This article investigates under which conditions instantiation-based proof procedures can be combined in a nested way, in order to mechanically construct new instantiation procedures for richer theories. Interesting applications in the field of verification are emphasized, particularly for handling extensions of the theory of arrays.

This paper relates the well-known Linear Temporal Logic with the logic of propositional schemata introduced in elsewhere by the authors. We prove that LTL is equivalent to a class of schemata in the sense that polynomial-time reductions exist from one logic to the other. Some consequences about complexity are given. We report about first experiments and the consequences about possible improvements in existing implementations are analyzed.

We define a logic of propositional formula schemata adding to the syntax of propositional logic indexed propositions and iterated connectives ranging over intervals parameterized by arithmetic variables. The satisfiability problem is shown to be undecidable for this new logic, but we introduce a very general class of schemata, called bound-linear, for which this problem becomes decidable. This result is obtained by reduction to a particular class of schemata called regular, for which we provide a sound and complete terminating proof procedure. This schemata calculus allows one to capture proof patterns corresponding to a large class of problems specified in propositional logic. We also show that the satisfiability problem becomes again undecidable for slight extensions of this class, thus demonstrating that bound-linear schemata represent a good compromise between expressivity and decidability.

International audience

Looking at inference as a way of transforming information so as to make it more easily usable (or interpretable) allows to consider accepted and rejected propositions as equally relevant and naturally gives a bipolar view of reasoning. The four possibilities of transforming information from accepted or rejected propositions into accepted or rejected ones are analyzed and examples illustrating them are given. This analysis is not only interesting per se but can also be useful in increasing capabilities of existing theorem provers. A unified framework based on former work by the authors is extended by incorporating the idea of theory-anti-subsumption related to Plotkin's generalization. Working on some technical details of this framework should allow automated reasoning tools to deal with different ways of connecting accepted and rejected propositions. © 2008 Wiley Periodicals, Inc.

We define a new class of rewrite systems operating over term-graphs. Our aim is twofold. First we propose to extend classical first-order rewrite rules in order to process easily data-structures with pointers (e.g., circular lists, doubly linked lists etc). For that, our rules provide specific features such as pointer (edges) redirections, relabeling of existing nodes etc. Unfortunately, such features are very often source of non confluence. Our second aim is then to ensure confluence of the considered rewrite systems in the new class. We introduce the notion of term-graphs with priority and show that orthogonal rewrite systems are confluent in our setting

A method for building finite models is proposed. It combines enumeration of the set of interpretations on a finite domain with strategies in order to prune significantly the search space. The main new ideas underlying our method are to benefit from symmetries and from the information extracted from the structure of the problem and from failures of model verification tests. The algorithms formalizing the approach are given and the standard properties (termination, completeness, and soundness) are proven. The method can deal with first-order logic with equality. In contrast to existing ones, it does not require to transform the initial problem into a normal form and can be easily extended to other logics. Experimental results and comparisons with related works are reported.

The use of regular tree grammars to represent and build models of formulae of first-order logic without equality is investigated. The combination of regular tree grammars with equational constraints provides a powerful and general way of representing Herbrand models. We show that the evaluation problem (i.e. the problem of finding the truth value of a formula in a given model) is decidable when models are represented in the way we propose. We also define a method to build such representations of models for first-order formulae. These results are a powerful extension of our former method for simultaneous search for refutations and models.