-
Simulation Logic, Applets and Compositional Verification
We present a compositional verification method for control flow based safety properties of smart card applets. Our method rests on a close correspondence between... -
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... -
Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems
Model-checking is a popular technique for verifying finite-state concurrent systems, the behaviour of which can be modeled using Labeled Transition Systems (Ltss). In... -
Specification and Verification of a Dynamic Reconfiguration Protocol for Agen...
Dynamic reconfiguration increases the availability of distributed applications by allowing them to evolve at run-time. This paper deals with the formal specification... -
Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus
Model-checking is a successful technique for automatically verifying concurrent finite-state systems. When building a model-checker, a good compromise must be made... -
Efficient Diagnostic Generation for Boolean Equation Systems
Boolean Equation Systems (BESs) provide a useful framework for the verification of concurrent finite-state systems. In practice, it is desirable that a BES resolution... -
Advanced Modelling and Verification Techniques Applied to a Cluster File System
This report describes the application of elaborated formal modelling techniques and tools from the CADP toolset for LOTOS to the validation of CFS, a distributed file... -
Validation of the Link Layer Protocol of the IEEE-1394 Serial Bus («FireWire»...
This paper deals with the description in E-LOTOS of the asynchronous LINK layer protocol of the IEEE-1394 Standard and its verification using model-checking. The... -
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... -
Uniform Strategies
We consider turn-based game arenas for which we investigate uniformity properties of strategies. These properties involve bundles of plays, that arise from some... -
Counting CTL
The original publication is available at www.springerlink.com. -
Counting LTL
The original publication is available at ieeexplore.ieee.org. -
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... -
Learning Transition Rules from Temporal Logic Properties
Most of the work on temporal representation issues in Machine Learning deals with the problem of learning/mining temporal patterns from a large set of temporal data.... -
Abstraction over Public Interfaces
The use of public interfaces as a means of encapsulating method implementations has become standard in software design, but still requires the development of... -
Factorising temporal specifications
This paper proposes a method to factorise the verification of temporal properties for multi-threaded programs over groups of different threads. Essentially, the method... -
Embedding of biological regulatory networks and property preservation
International audience -
Temporal Logic To Query Semantic Graphs Using The Model Checking Method
International audience -
Counting CTL
34 pages
