15 Jun
2015
15 Jun
'15
2:37 p.m.
I am happy to announce that the following two papers have been
accepted at the 22nd International SPIN Symposium on Model Checking of
Software (SPIN 2015) to be held in Stellenbosch, South Africa on 24–26
August 2015.
---
On Refinement of Büchi Automata for Explicit Model Checking
František Blahoudek¹, Alexandre Duret-Lutz²,
Vojtěch Rujbr¹, and Jan Strejček¹
¹Faculty of Informatics, Masaryk University, Brno, Czech Republic
²LRDE, EPITA, Le Kremlin-Bicêtre, France
https://www.lrde.epita.fr/wiki/Publications/blahoudek.15.spin
Abstract:
In explicit model checking, systems are typically described in an
implicit and compact way. Some valid information about the system
can be easily derived directly from this description, for example
that some atomic propositions cannot be valid at the same time. The
paper shows several ways to apply this information to improve the
Büchi automaton built from an LTL specification. As a result, we get
smaller automata with shorter edge labels that are easier to
understand andmore importantly, for which the explicit model
checking process performs better.
---
Practical Stutter-Invariance Checks for ω-Regular Languages
Thibaud Michaud and Alexandre Duret-Lutz
LRDE, EPITA, Le Kremlin-Bicêtre, France
https://www.lrde.epita.fr/wiki/Publications/michaud.15.spin
Abstract:
We propose several automata-based constructions that check whether a
specification is stutter-invariant. These constructions assume that
a specification and its negation can be translated into Büchi
automata, but aside from that, they are independent of the
specification formalism. These transformations were inspired by a
construction due to Holzmann and Kupferman, but that we broke down
into two operations that can have different realizations, and that
can be combined in different ways. As it turns out, implementing
only one of these operations is needed to obtain a functional
stutter-invariant check. Finally we have implemented these
techniques in a tool so that users can easily check whether an LTL
or PSL formula is stutter-invariant.
--
Alexandre Duret-Lutz
20 Jun
20 Jun
9:05 a.m.
New subject: publications: two papers accepted at ATVA'16
I am happy to announce that the following two papers have been
accepted at the 14th International Symposium on Automated Technology
for Verification and Analysis (ATVA 2016) to be held in Chiba, Japan on
17-19 October 2016.
—
Heuristics for Checking Liveness Properties with Partial Order Reductions
A. Duret-Lutz(1), F. Kordon(2,3), D. Poitrenaud(3,4), E. Renault(1)
(1) LRDE, EPITA, Kremlin-Bicêtre, France
(2) Sorbonne Universités, UPMC Univ. Paris 06, France
(3) CNRS UMR 7606, LIP6, F-75005 Paris, France
(4) USPC, Université Paris Descartes, Paris, France
https://www.lrde.epita.fr/wiki/Publications/duret.16.atva
Abstract:
Checking liveness properties with partial-order reductions requires
a cycle proviso to ensure that an action cannot be
postponed forever. The proviso forces each cycle to contain at
least one fully expanded state. We present new heuristics to select
which state to expand, hoping to reduce the size of the resulting graph.
The choice of the state to expand is done when encountering a
dangerous edge. Almost all existing provisos expand the source of this edge,
while this paper also explores the expansion of the destination and the
use of SCC-based information.
—
Spot 2.0 — a framework for LTL and ω-automata manipulation
Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne
Renault, and Laurent Xu
LRDE, EPITA, Kremlin-Bicêtre, France
https://www.lrde.epita.fr/wiki/Publications/duret.16.atva2
Abstract:
We present Spot 2.0, a C++ library with Python bindings and an assortment of
command-line tools designed to manipulate LTL and ω-automata in batch.
New automata-manipulation tools were introduced in Spot 2.0; they support
arbitrary acceptance conditions, as expressible in the Hanoi Omega Automaton
format. Besides being useful to researchers who have automata to process, its
Python bindings can also be used in interactive environments to teach ω-automata
and model checking.
10:38 a.m.
New subject: publications: two papers accepted at ATVA'16
Félicitations !
-----Message d'origine-----
De : Annonce [mailto:annonce-bounces@lrde.epita.fr] De la part de Etienne Renault
Envoyé : lundi 20 juin 2016 09:06
À : annonce(a)lrde.epita.fr
Objet : [Lrde Annonce] publications: two papers accepted at ATVA'16
I am happy to announce that the following two papers have been accepted at the 14th
International Symposium on Automated Technology for Verification and Analysis (ATVA 2016)
to be held in Chiba, Japan on
17-19 October 2016.
—
Heuristics for Checking Liveness Properties with Partial Order Reductions
A. Duret-Lutz(1), F. Kordon(2,3), D. Poitrenaud(3,4), E. Renault(1)
(1) LRDE, EPITA, Kremlin-Bicêtre, France
(2) Sorbonne Universités, UPMC Univ. Paris 06, France
(3) CNRS UMR 7606, LIP6, F-75005 Paris, France
(4) USPC, Université Paris Descartes, Paris, France
https://www.lrde.epita.fr/wiki/Publications/duret.16.atva
Abstract:
Checking liveness properties with partial-order reductions requires
a cycle proviso to ensure that an action cannot be
postponed forever. The proviso forces each cycle to contain at
least one fully expanded state. We present new heuristics to select
which state to expand, hoping to reduce the size of the resulting graph.
The choice of the state to expand is done when encountering a
dangerous edge. Almost all existing provisos expand the source of this edge,
while this paper also explores the expansion of the destination and the
use of SCC-based information.
—
Spot 2.0 — a framework for LTL and ω-automata manipulation
Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne
Renault, and Laurent Xu
LRDE, EPITA, Kremlin-Bicêtre, France
https://www.lrde.epita.fr/wiki/Publications/duret.16.atva2
Abstract:
We present Spot 2.0, a C++ library with Python bindings and an assortment of
command-line tools designed to manipulate LTL and ω-automata in batch.
New automata-manipulation tools were introduced in Spot 2.0; they support
arbitrary acceptance conditions, as expressible in the Hanoi Omega Automaton
format. Besides being useful to researchers who have automata to process, its
Python bindings can also be used in interactive environments to teach ω-automata
and model checking.
_______________________________________________
Annonce mailing list
Annonce(a)lrde.epita.fr
https://lists.lrde.epita.fr/listinfo/annonce
2860
days inactive
3231
days old
2 comments
3 participants
participants (3)
-
Alexandre Duret-Lutz -
Etienne Renault -
joel courtois