9 citations · 23 across the 8 of their papers we have counts for
8 papers
Simplifying LTL Model Checking Given Prior Knowledge
Alexandre Duret-Lutz, Denis Poitrenaud, Yann Thierry-Mieg
We consider the problem of the verification of an LTL specification on a system given some prior knowledge , an LTL formula that is known to satisfy. The automata-th…
Structural Reductions and Stutter Sensitive Properties
Emmanuel Paviot-Adet, Denis Poitrenaud, Etienne Renault +1
Verification of properties expressed as -regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However proper…
LTL under reductions with weaker conditions than stutter-invariance
Emmanuel Paviot-Adet, Denis Poitrenaud, Etienne Renault +1
Verification of properties expressed as-regular languages such as LTL can benefit hugely from stutter-insensitivity, using a diverse set of reduction strategies. However properties…
Symbolic and Structural Model-Checking
Yann Thierry-Mieg
Brute-force model-checking consists in exhaustive exploration of the state-space of a Petri net, and meets the dreaded state-space explosion problem. In contrast, this paper shows…
Modeling a Cache Coherence Protocol with the Guarded Action Language
Quentin L. Meunier, Yann Thierry-Mieg, Emmanuelle Encrenaz
We present a formal model built for verification of the hardware Tera-Scale ARchitecture (TSAR), focusing on its Distributed Hybrid Cache Coherence Protocol (DHCCP). This protocol…
Model Checking Contest @ Petri Nets, Report on the 2013 edition
Fabrice Kordon, Alban Linard, Marco Beccuti +14
This document presents the results of the Model Checking Contest held at Petri Nets 2013 in Milano. This contest aimed at a fair and experimental evaluation of the performances of…