LOZES , Etienne

The recent interest for specification on resources yields so-called spatial logics, that is specification languages offering spatial connectives: a separation into two subcomponents of the considered structure, (* ,or |), and its adjunct, the guarantee respect to the extension of the structure (− * ,). We consider two resource models and their...

International audience

A system of communicating finite state machines is synchronizable [1, 4] if its send trace semantics, i.e. the set of sequences of sendings it can perform, is the same when its communications are FIFO asynchronous and when they are just rendezvous synchronizations. This property was claimed to be decidable in several conference and journal...

A system of communicating finite state machines is synchronizable if its send trace semantics, i.e.the set of sequences of sendings it can perform, is the same when its communications are FIFO asynchronous and when they are just rendez-vous synchronizations. This property was claimed to be decidable in several conference and journal papers for...

Recent trends in formal models of web services description languages and session types focus on the asynchronicity of communications. In this paper, we study a core of these models that arose from our modelling of the Sing# programming language, and demonstrate correspondences between Sing# contracts, asynchronous session behaviors, and the...

A system of communicating finite state machines is synchronizable [1, 4] if its send trace semantics, i.e. the set of sequences of sendings it can perform, is the same when its communications are FIFO asynchronous and when they are just rendezvous synchronizations. This property was claimed to be decidable in several conference and journal...

Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed λ-calculus into the modal µ-calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely...

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

We study the relationship between two kinds of higher-order extensions of model checking: HORS model checking, where models are extended to higher-order recursion schemes, and HFL model checking , where the logic is extended to higher-order modal fixpoint logic. These extensions have been independently studied until recently, and the former has...

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 Ambient Logic (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. In this paper, we study the expressiveness of AL. We define formulas for capabilities and for communication in MA. We also derive some formulas that capture...

The Ambient Logic (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. We study some basic questions concerning the discriminating power of AL, focusing on the equivalence on processes induced by the logic (=L). As underlying...

International audience

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

In this paper, we work on the notion of k-synchronizability: a system is k-synchronizable if any of its executions, up to reordering causally independent actions, can be divided into a succession of k-bounded interaction phases. We show two results (both for mailbox and peer-to-peer automata): first, the reachability problem is decidable for...

A communicating system is k-synchronizable if all of the message sequence charts representing the executions can be divided into slices of [Formula: see text] sends followed by k receptions. It was previously shown that, for a fixed given k, one could decide whether a communicating system is k-synchronizable. This result is interesting because...

International audience

Process equivalences are formal methods that relate programs and systems which, informally, behave in the same way. Since there is no unique notion of what it means for two dynamic systems to display the same behaviour there are a multitude of formal process equivalences, ranging from bisimulation to trace equivalence, categorised in the...

We study k-synchronizability: a system is k-synchronizable if any of its executions, up to reordering causally independent actions, can be divided into a succession of k-bounded interaction phases. We show two results (both for mailbox and peer-to-peer automata): first, the reachability problem is decidable for k-synchronizable systems; second,...

Futures and promises are respectively a read-only and a write-once pointer to a placeholder in memory. They are used to transfer information between threads in the context of asynchronous concurrent programming. Futures and promises simplify the implementation of synchronisation mechanisms between threads. Nonetheless they can be error prone as...

International audience

International audience

Communicating finite-state machines (CFMs) are a Turing powerful model of asynchronous message-passing distributed systems. In weakly synchronous systems, processes communicate through phases in which messages are first sent and then received, for each process. Such systems enjoy a limited form of synchronization, and for some communication...

There is a wide variety of message-passing communication models, ranging from synchronous "rendez-vous" communications to fully asynchronous/out-of-order communications. For large-scale distributed systems, the communication model is determined by the transport layer of the network, and a few classes of orders of message delivery (FIFO,...