Annonce August 2015

annonce@lrde.epita.fr

1 participants
2 discussions

publications: two papers accepted at Spin'15
by Alexandre Duret-Lutz 20 Jun '16

20 Jun '16

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

3 2

nouvelle publication
by Souheib Baarir 31 Aug '15

31 Aug '15

I am happy to announce that the following paper has been accepted in the International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR’15) : SAT-based Minimization of Deterministic ω-Automata Souheib Baarir and Alexandre Duret-Lutz. LRDE, EPITA, Le Kremlin-Bicêtre, France A+, Soheib.

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Annonce August 2015