ABSTRACT. The development of the logic of bunched implications, BI, together with its somewhat characteristic resource semantics, led to the formulation of Separation Logic, which forms the basis of the Infer program analyser deployed in Facebook's code production. This rather successful story sits within a broader, quite systematic logical context. I will review the (family of) logics, including process logics, that are supported by resource semantics, explaining their more-or-less uniform meta-theoretic basis and illustrating their uses in a range of modelling applications, including access control, systems security, and workflow simulation. 

ABSTRACT. In previous work we presented the flow framework for verifying complex concurrent data structures using separation logic (SL). The framework enables the decomposition of the overall correctness proof of the data structure into (1) a proof of an abstract template algorithm that captures the underlying synchronization protocol between data structure operations, and (2) a refinement proof of this template to the concrete data structure implementation. In this paper, we investigate the automation of proofs expressed in this framework. We use the give-up template for concurrent dictionaries, and an implementation of this template based on B+ trees as a case study. We detail the challenges in automating the framework and present a revised version geared towards automation in a standard SL-based symbolic execution engine. We have implemented such an engine in the deductive verification tool GRASShopper and used it to mechanize the proof of our case study. Our experience suggests that the flow framework can express simple correctness proofs of complex concurrent data structures and can be automated using off-the-shelf verification tools, requiring only minor extensions to standard reasoning engines for SL.

ABSTRACT. We propose the strong wand and the Factor rule in a cyclic-proof system for the separation-logic entailment checking problem with general inductive predicates. The strong wand is similar to but stronger than the magic wand and is defined syntactically. The Factor rule, which uses the strong wand, is an inference rule for spatial factorization to expose an implicitly allocated cell in inductive predicates. By this rule, we can void getting stuck in the Unfold-Match-Remove strategy. We show a semi-decision algorithm of proof search in the cyclic-proof system with the Factor rule and the experimental results of its prototype implementation.

ABSTRACT. Separation Logic (SL) is a logical formalism for reasoning about programs that use pointers to mutate data structures. SL has proven itself successful in the field of program verification over the past fifteen years as an assertion language to state properties about memory heaps using Hoare triples. Since the full logic is not recursively enumerable, most of the proof-systems and verification tools for SL focus on the decidable but rather restricted symbolic heaps fragment. Moreover, recent proof-systems that go beyond symbolic heaps allow either the full set of connectives, or the definition of arbitrary predicates, but not both. In this work, we present a labelled proof-system called GM SL that allows both the definition of arbitrary inductive predicates and the full set of SL connectives.

ABSTRACT. We consider basic symbolic heaps, i.e. symbolic heaps without any inductive predicates, but within a memory model featuring permissions. We propose a complete proof system for this logic that is entirely independent of the permission model. This is an ongoing work towards a complete proof system for symbolic heaps with lists, and more generally towards a proof theory of permissions in separation logics with recursive predicates and Boolean BI with abstract predicates.

ABSTRACT. To adequately define the semantics of multithreaded programs, modern revisions of programming languages, such as C/C++ and Java, have adopted weak memory consistency models, which allow more program behaviours than can be observed by simply interleaving the threads of the program. Most computer scientists consider weak memory consistency as being an extremely complicated concept, and one better left only to a small circle of experts to master.

Yet, we show that weak memory is not that complicated. Using separation logic triples, we can not only provide concise explanations of the various constructs of the C/C++11 memory models, but these explanations are also sufficient for verifying the most important synchronisation patterns appearing in real-world concurrent programs.

ABSTRACT. We investigate the complexity consequences of adding pointer arithmetic to separation logic. Specifically, we study an extension of the points-to fragment of symbolic-heap separation logic with sets of simple "difference constraints" of the form x <= y + k, where x and y are pointer variables and k is an integer offset. This extension can be considered a practically minimal language for separation logic with pointer arithmetic.

Most significantly, we find that, even for this minimal language, polynomial-time decidability is already impossible: satisfiability becomes NP-complete, while quantifier-free entailment becomes CoNP-complete and quantified entailment becomes \Pi^P_2-complete (where \Pi^P_2 is the second class in the polynomial-time hierarchy).

However, the language does satisfy the small model property, meaning that any satisfiable formula A has a model of size polynomial in A, whereas this property fails when richer forms of arithmetical constraints are permitted.

ABSTRACT. We first show that infinite satisfiability can be reduced to finite satisfiability for all prenex formulas of Separation Logic with $k\geq1$ selector fields ($\seplogk{k}$). Second, we show that this entails the decidability of the finite and infinite satisfiability problem for the class of prenex formulas of $\seplogk{1}$, by reduction to the first-order theory of one unary function symbol and unary predicate symbols. We also prove that the complexity is not elementary, by reduction from the first-order theory of one unary function symbol. Finally, we prove that the Bernays-Sch\"onfinkel-Ramsey fragment of prenex $\seplogk{1}$ formulae with quantifier prefix in the language $\exists^*\forall^*$ is \pspace-complete. The definition of a complete (hierarchical) classification of the complexity of prenex $\seplogk{1}$, according to the quantifier alternation depth is left as an open problem.

ABSTRACT. We present Sloth, a solver for separation logic modulo theory constraints specified in the separation logic SL∗, a propositional separation logic that we recently introduced in our IJCAR'18 paper "A Separation Logic with Data: Small Models and Automation." SL∗ admits NP decision procedures despite its high expressiveness; features of the logic include support for list and tree fragments, universal data constraints about both lists and trees, and Boolean closure of spatial formulas. Sloth solves SL* constraints via an SMT encoding of SL* that is based on the logic's small-model property. We argue that, while clearly still a work in progress, Sloth already demonstrates that SL* lends itself to the automation of nontrivial examples. These results complement the theoretical work presented in the IJCAR'18 paper.

ABSTRACT. TBA