DEMRI , Stéphane

We present a general approach to axiomatise separation logics with heaplet semantics with no external features such as nominals/labels. To start with, we design the first (internal) Hilbert-style axiomatisation for the quantifier-free separation logic SL(*, −*). We instantiate the method by introducing a new separation logic with essential...

The list segment predicate ls used in separation logic for verifying programs with pointers is well-suited to express properties on singly-linked lists. We study the effects of adding ls to the full quantifier-free separation logic with the separating conjunction and implication, which is motivated by the recent design of new fragments in which...

The list segment predicate ls used in separation logic for verifying programs with pointers is well-suited to express properties on singly-linked lists. We study the effects of adding ls to the full quantifier-free separation logic with the separating conjunction and implication, which is motivated by the recent design of new fragments in which...

Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this paper, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an...

We present the first complete axiomatisation for quantifier-free separation logic. The logic is equipped with the standard concrete heaplet semantics and the proof system has no external feature such as nominals/labels. It is not possible to rely completely on proof systems for Boolean BI as the concrete semantics needs to be taken into...