-
Logiques temporelles basées sur actions pour la vérification des systèmes asy...
La vérification formelle est indispensable pour assurer la fiabilité des applications complexes et critiques comme les protocoles de télécommunication et les systèmes... -
A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems
Boolean Equation Systems are a useful formalism for modeling various verification problems of finite-state concurrent systems, in particular the equivalence checking... -
On Combining Functional Verification and Performance Evaluation using CADP
Considering functional correctness and performance evaluation in a common framework is desirable, both for scientific and economic reasons. In this report, we describe... -
Synthesising Labelled Transitions and Operational Congruences in Reactive Sys...
The dynamics of process calculi, e.g. CCS, have often been defined using a labelled transition system (LTS). More recently it has become common when defining dynamics... -
Synthesising Labelled Transitions and Operational Congruences in Reactive Sys...
This paper is the second in a series of two. It relies on its companion, Part 1, to motivate the central problem addressed by the series, namely: how to synthesise... -
SVL : a Scripting Language for Compositional Verification
Compositional verification is a way to avoid state explosion for the enumerative verification of complex concurrent systems. Process algebras such as Lotos are... -
A Bisimulation for the Blue Calculus
The Blue calculus is a direct extension of both the lambda and the pi calculi. In this report, we define an equivalence for this calculus based on barbed congruence,... -
An Asynchronous Model of Locality, Failure, and Process Mobility
We present a model of distributed computation which is based on a fragment of the $\pi$-calculus relying on {\em asynchronous} communication. We enrich the model with... -
Formal Description and Analysis of a Bounded Retransmission Protocol
This paper reports about the formal specification and verification of a Bounded Retransmission Protocol (BRP) used by Philips in one of its products. We started with... -
On Bisimulations for the Asynchronous pi-calculus
The {\em asynchronous $\pi$-calculus\/} is a variant of the $\pi$-calculus where message emission is non-blocking. Honda and Tokoro have studied a semantics for this... -
Some Congruence Properties for pi-calculus Bisimilarities
Both for interleaving and for non-interleaving semantics, several variants of a $\pi$-calculus bisimilarity can be given which differ on the requirements imposed on... -
Lazy functions and mobile processes
This paper continues the study of Milner's encoding of the lazy $\lambda$-calculus into the $\pi$-calculus \cite{Mil92}. The encoding is shown to give rise to a... -
Bisimulation for higher-order process calculi
A higher-order process calculus is a calculus for communicating systems which contains higher-order constructs like communication of terms. We analyse the notion of... -
Action Emulation
International audience -
An overview of CADP 2001
CADP is a toolbox for specifying and verifying asynchronous finite-state systems described using process algebraic languages. It offers a wide range of... -
Typing Noninterference for Reactive Programs
We propose a type system to enforce the security property of noninterference in a core reactive language, obtained by extending the imperative language of Volpano,... -
Behavioural Theory for Mobile Ambients
We study a behavioural theory of Cardelli and Gordon's Mobile Ambients, a process calculus for modelling mobile agents in wide-area networks, focussing on reduction... -
CAESAR_SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free...
Boolean Equation Systems (BESs) provide a useful framework for modeling various verification problems on finite-state concurrent systems, such as equivalence checking... -
Modélisation et analyse de systèmes asynchrones avec CADP
La conception des systèmes industriels critiques comportant du parallélisme asynchrone nécessite l'utilisation de méthodes formelles, assistées par des outils de...
