Yann Thierry-Mieg

In Proceedings of the 41th IFIP international conference on formal techniques for distributed objects, components and systems (FORTE’22)

Abstract Verification of properties expressed as omega-regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However properties that are not stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter insensitivity.

Symbolic model checking of stutter invariant properties using generalized testing automata

By Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, Yann Thierry-Mieg

2014-04-01

In Proceedings of the 20th international conference on tools and algorithms for the construction and analysis of systems (TACAS’14)

Abstract In a previous work, we showed that a kind of $\omega$-automata known as Transition-based Generalized Testing Automata (TGTA) can outperform the Büchi automata traditionally used for explicit model checking when verifying stutter-invariant properties. In this work, we investigate the use of these generalized testing automata to improve symbolic model checking of stutter-invariant LTL properties. We propose an efficient symbolic encoding of stuttering transitions in the product between a model and a TGTA.

Self-loop aggregation product — a new hybrid approach to on-the-fly LTL model checking

By Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg

2011-06-23

In Proceedings of the 9th international symposium on automated technology for verification and analysis (ATVA’11)

Abstract We present the Self-Loop Aggregation Product (SLAP), a new hybrid technique that replaces the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed product is an explicit graph of aggregates (symbolic sets of states) that can be interpreted as a Büchi automata. The criterion used by SLAP to aggregate states from the Kripke structure is based on the analysis of self-loops that occur in the Büchi automaton expressing the property to verify.

Combining explicit and symbolic approaches for better on-the-fly LTL model checking

By Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg

2011-06-01

In

Abstract We present two new hybrid techniques that replace the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed products are explicit graphs of aggregates (symbolic sets of states) that can be interpreted as Büchi automata. These hybrid approaches allow on the one hand to use classical emptiness-check algorithms and build the graph on-the-fly, and on the other hand, to have a compact encoding of the state space thanks to the symbolic representation of the aggregates.

Building efficient model checkers using hierarchical set decision diagrams and automatic saturation

By Alexandre Hamez, Yann Thierry-Mieg, Fabrice Kordon

2009-08-01

In Fundamenta Informaticae

Abstract Shared decision diagram representations of a state-space provide efficient solutions for model-checking of large systems. However, decision diagram manipulation is tricky, as the construction procedure is liable to produce intractable intermediate structures (a.k.a peak effect). The definition of the so-called saturation method has empirically been shown to mostly avoid this peak effect, and allows verification of much larger systems. However, applying this algorithm currently requires deep knowledge of the decision diagram data-structures.

Hierarchical set decision diagrams and automatic saturation

By Alexandre Hamez, Yann Thierry-Mieg, Fabrice Kordon

2008-03-01

In Petri nets and other models of concurrency –ICATPN 2008

Abstract Shared decision diagram representations of a state-space have been shown to provide efficient solutions for model-checking of large systems. However, decision diagram manipulation is tricky, as the construction procedure is liable to produce intractable intermediate structures (a.k.a peak effect). The definition of the so-called saturation method has empirically been shown to mostly avoid this peak effect, and allows verification of much larger systems. However, applying this algorithm currently requires deep knowledge of the decision diagram data-structures, of the model or formalism manipulated, and a level of interaction that is not offered by the API of public DD packages.

libDMC: A library to operate efficient distributed model checking

By Alexandre Hamez, Fabrice Kordon, Yann Thierry-Mieg

2007-03-13

In Workshop on performance optimization for high-level languages and libraries — associated to IPDPS’2007

Abstract Model checking is a formal verification technique that allows to automatically prove that a system’s behavior is correct. However it is often prohibitively expensive in time and memory complexity, due to the so-called state space explosion problem. We present a generic multi-threaded and distributed infrastructure library designed to allow distribution of the model checking procedure over a cluster of machines. This library is generic, and is designed to allow encapsulation of any model checker in order to make it distributed.

LTL under reductions with weaker conditions than stutter invariance

Symbolic model checking of stutter invariant properties using generalized testing automata

Self-loop aggregation product — a new hybrid approach to on-the-fly LTL model checking

Combining explicit and symbolic approaches for better on-the-fly LTL model checking

Building efficient model checkers using hierarchical set decision diagrams and automatic saturation

Hierarchical set decision diagrams and automatic saturation

libDMC: A library to operate efficient distributed model checking

Search

Tags