2 May
2018
2 May
'18
2:54 p.m.
========================================================================
Séminaire MeFoSyLoMa
http://www.mefosyloma.fr/
Méthodes Formelles pour les Systèmes Logiciels et Matériels
vendredi 18 mai 2018, 14h-16h30
Adresse:
Amphi IP 11
24 rue Pasteur, 94270 Le Kremlin-Bicêtre
Métro Porte d'Italie
Plans d'accès :
https://www.google.com/maps?q=48.815378,2.363106
https://www.lrde.epita.fr/~adl/img/plan-ip11.png
S'il y en a parmi vous qui comptent venir en voiture, le parking du
centre commercial Okabé est gratuit pendant 3h.
http://www.okabe.com/okabe/fr/okabe-parking
========================================================================
Le séminaire MeFoSyLoMa est animé conjointement par les laboratoires
Cedric (Cnam), IBISC (Univ. Evry), LACL (Univ. Paris 12), LIP6 (UPMC),
LIPN (Univ. Paris 13), LRDE (Epita), LSV (École Normale Supérieure de
Cachan) et LTCI (TELECOM ParisTech). Son objet est de permettre la
confrontation de différentes approches ou points de vue sur
l'utilisation des méthodes formelles dans les domaines du génie
logiciel, de la conception de circuit, des systèmes répartis, des
systèmes temps-réel ou encore des systèmes d'information. Il
s'organise autour de réunions bimestrielles où sont exposés des
travaux de recherche récents sur ce thème.
========================================================================
Programme
14h00-15h00: Étienne Renault (LRDE/EPITA),
"The quest for an efficient LTL model-checking"
Abstract: Model checking is an automated verification technique
that is used for establishing that a model of a system is correct
with respect to some given specification. One of the most serious
problems with model checking in practice is the so-called "state
explosion problem", i.e the state-space of a system can be too large
to be processed in a reasonable time and to be stored on the
memory. This problem can be addressed using symbolic or explicit
techniques. In this talk I will focus on the latter one by
overviewing the recent advances in (1) emptiness checks and (2)
partial-order reductions.
15h00-15h30: Mathias Ramparison (LIPN, Université Paris 13),
"Timed automata with parametric updates"
Abstract: Timed automata (TAs) represent a powerful formalism to
model and verify systems where concurrency is intricated with hard
timing constraints. However, they can seem limited when dealing with
uncertain or unknown timing constants. Several parametric extensions
were proposed in the literature, and the vast majority of them leads
to the undecidability of the EF-emptiness problem: "is the set of
valuations reaching a given location empty?" Here, we study an
extension of TAs where clocks can be updated to a parameter. While
the EF-emptiness problem is undecidable for rational-valued
parameters, it becomes PSPACE-complete for integer-valued
parameters. In addition, exact synthesis of the parameter valuations
set can be achieved. We also extend these two results to the
EF-universality ("are all valuations reaching a given location?"),
AF-emptiness ("is the set of valuations such that a given location
is unavoidable empty?") and AF-universality ("are all valuations
such that a given location is unavoidable?") problems. 15h30-16h00:
pause café 16h00-16h30: vie du groupe
15h30-16h00: pause café
16h00-16h30: vie du groupe
========================================================================
--
Alexandre Duret-Lutz
