-
On Post’s embedding problem and the complexity of lossy channels
Lossy channel systems were originally introduced to model communication protocols. It gave birth to a complexity class wich remained scarcely undersood for a long... -
Contracts and Behavioral Patterns for Systems of systems: The EU IP DANSE app...
This report presents some of the results of the first year of Danse, one of the first EU IP projects dedicated to System of Systems. Concretely, we offer a tool chain... -
Distributed On-the-Fly Verification of Large State Spaces
The verification of concurrent finite-state systems is confronted in practice with the state explosion problem (prohibitive size of the underlying state space), which... -
Vérification de systèmes paramétrés avec Cubicle
International audience -
Verification of real time properties in fiacre language
The formal verification of critical, reactive systems is a very complicated task, especially for non experts. In this work, we more particularly address the problem of... -
Temporal Logic To Query Semantic Graphs Using The Model Checking Method
International audience -
Validation of a New Functional Design of Automatic Protection Systems at Leve...
International audience -
Behavior Analysis of Malicious Code by Weighted Behavior Abstraction
This work is a weighted generalization of the abstraction based analysis technique we previously proposed for the detection of high-level malware behaviors. Our... -
Uniform Random Sampling of Traces in Very Large Models
This paper presents some first results on how to perform uniform random walks (where every trace has the same probability to occur) in very large models. The models... -
Parallel and distributed high-level colored Petri net model checking
This thesis enters in the frame of the automatic verification of concurrent software based on an intermediary formal language : high-level colored Petri nets. We... -
Model checking : éléments de base
This dataset has no description
-
Formal Verification of Distributed Algorithms using PlusCal-2
Designing sound algorithms for concurrent and distributed systems is subtle and challenging. These systems are prone to deadlocks and race conditions, which occur in... -
Formal approaches for performability analysis of communicating systems : an a...
We are interested in analyzing the performability requirements of mobile communication systems by using model checking techniques. We model these systems using a... -
An assertions-based approach to verifying the absence property pattern
International audience -
Vérification formelle et robots mobiles
International audience -
Convex invariant refinement by control node splitting: a heuristic approach
International audience -
Towards an integrative approach for the modeling and formal verification of b...
The study of large models of biological networks by means of analysis and simulation tools leads to large amounts of predictions. This raises the question of how to... -
Static Analysis using Parameterised Boolean Equation Systems
Submitted to an international 2006 conference -
KEDGEN2: A key establishment and derivation protocol for EPC Gen2 RFID systems
International audience -
Model Checking using Generalized Testing Automata
International audience
