ABSTRACT. Over-approximating (OX) program logics, such as separation logic (SL),are used to verify properties of heap-manipulating programs: allterminating behaviour is characterised, but the reported results anderrors need not be reachable. OX function specifications are thusincompatible with true bug-finding supported by symbolic executiontools such as Pulse and Gillian. In contrast, under-approximating (UX)program logics, such as incorrectness separation logic (ISL), are usedto find true results and bugs: reported results and errors arereachable, but not all behaviour can be characterised. UX functionspecifications thus cannot capture full verification.We introduce exact separation logic (ESL) for reasoning aboutheap-manipulating sequential programs, which provides fully verifiedfunction specifications compatible with true bug finding: allterminating behaviour is captured in full, and all reported resultsand errors are reachable.  ESL supports mutually recursive functions,which require subtle definitions of internal and external functionspecifications compared with the familiar definitions for OX logics.We prove a frame-preserving soundness result for ESL, and ISL and SL,thus demonstrating functional compositionality of UX reasoning. Weverify exact specifications of list algorithms using standardinductive predicates, observing the difference between abstractionwhich hides information and OX reasoning which looses information.  Weintroduce a symbolic execution semantics that can call functions withESL specifications, and prove a backwards completeness result thatdemonstrates that verified ESL function specifications are indeedcompatible with true bug-finding.

ABSTRACT. Two results are presented concerning the entailment problem in Separation Logic with inductively defined predicate symbols and theory reasoning. First, we show that the entailment problem is undecidable for rules satisfying the progress, connectivity and establishment conditions, if theory reasoning is considered. The result holds for a wide class of theories, even with a very low expressive power. For instance it applies to the natural numbers with the successor function, or with the usual order. Second, we show that every entailment problem can be reduced to an entailment problem containing no equality (neither in the formulas nor in the recursive rules defining the semantics of the predicate symbols).

ABSTRACT. In this paper, we define a temporal extension of Bunched Implication Logic (BI), called LTBI, that combines the LTL temporal connectives with BI connectives. After studying its semantics and illustrating its expressiveness, we design a labelled tableaux calculus for this new logic and then prove its soundness w.r.t. the Kripke-style semantics of LTBI. We finally discuss completeness issues of the calculus.

ABSTRACT. We compare the model-theoretic expressiveness of the symbolic heap fragment of Separation Logic (SL) with inductive definitions with (Monadic) Second Order Logic ((M)SO). While SL and MSO are incomparable on structures of unbounded treewidth, it turns out that SL can be embedded in SO and that MSO becomes a strict subset of SL, when the treewidth of the models is bounded by a constant and the relation symbols have arity one or two. We leave open the problems of equivalence between (M)SO and SL on bounded treewidth models over signatures containing relation symbols of arity three or more.

ABSTRACT. Concurrent separation logic (CSL) has demonstrated that separation logic is exceptionally well-suited for reasoning about concurrent programs. However, CSL on its own is not able to express and exploit the desired notion of functional correctness for concurrent data structures: linearizability. While CSL is regularly employed to *prove* linearizability, linearizability is an extra-logical notion: when working inside the separation logic, there is no way to make *use* of the fact that some data structure is linearizable. Therefore, the TaDA paper in 2014 proposed a new style of specifying concurrent data structures: *logically atomic Hoare triples*. These triples provide a simple way to turn a specification of a sequential data structure (say, a stack) into a concurrent variant of the same specification, stipulating that each operation must "behave atomically". This enables clients of logically atomic triples to make use of the "invariant rule", a key proof rule in CSL to reason about an atomic step of execution. In this talk, I will explain how logically atomic triples are used in Iris to specify and verify concurrent data structures as well as clients of these data structures. I will also show how logically atomic triples are defined inside the Iris program logic by composing lower-level logical primitives.

ABSTRACT. Logical atomicity has been widely accepted as a specification format for data structures in concurrent separation logic. While both lock-free and lock-based data structures have been verified against logically atomic specifications, most of the latter start with atomic specifications for the locks as well. In this paper, we compare this approach with one based on older lock-invariant-based specifications for locks. We show that we can still prove logically atomic specifications for data structures with fine-grained locking using these older specs, but the proofs are significantly more complicated than those that use atomic lock specifications. Our proof technique is implemented in the Verified Software Toolchain, which relies on older lock specifications for its soundness proof, and applied to C implementations of lock-based concurrent data structures.

ABSTRACT. Heap list is a data structure used by many implementations of memory allocators to organize the heap part of the program’s memory. Operations on heap lists employ pointer arithmetic and therefore, reasoning about the correctness of heap list implementations requires to deal simultaneously with pointer arithmetic inside the inductive definition specifying the heap list. In this work, we investigate decision problems for SLAH, a separation logic fragment that allows pointer arithmetic and an inductive definition for heap lists, thus enabling specification of properties for programs in memory allocators. Pointer arithmetic inside the inductive definition for heap lists is challenging for automated reasoning. We tackle this challenge and achieve decision procedures for both satisfiability and entailment of SLAH formulas. The crux of our decision procedure for satisfiability is to compute summaries of the inductive definition for heap lists. We show that although the summary is naturally expressed as an existentially quantified non-linear arithmetic formula, it can actually be transformed into an equivalent linear arithmetic formula. The decision procedure for entailment, on the other hand, has to match and split the spatial atoms according to the arithmetic relation between address variables. We report on the implementation of these decision procedures and their good performance in solving problems issued from the verification of building block programs manipulating heap-lists used in memory allocators.

ABSTRACT. We present a program logic for reasoning about heap space in a λ-calculus equipped with garbage collection and mutable state. Compared with prior work by Madiot and Pottier, we target a higher-level language. This requires us to introduce an assertion to reason about the roots held by the evaluation context.