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
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
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.