Français Anglais
Accueil Annuaire Plan du site
Accueil > Evenements > Séminaires
Séminaire d'équipe(s) ParSys
Recent Progress in Model Checking of Fault-tolerant Distributed Algorithms
Josef Widder

03 December 2015, 10h30
Salle/Bat : 465/PCRI-N
Contact :

Activités de recherche : Algorithmique distribuée

Résumé :
Computers are used in a wide range of applications, including
embedded control systems in cars and aircraft, cloud computing,
and the Internet. As we increasingly depend on the correct
operation of such systems, it becomes crucial to design them in a
way that ensures that they behave as expected. To do so, one has
to address two problem areas: on the one hand, partial failure
that is outside the control of a system designer (such as power
outages or bit-flips due to radiation), and on the other hand,
design faults (bugs). The former is classically addressed by
means of replication and fault-tolerant distributed algorithms,
while the latter is dealt with by rigorous software engineering
methods, such as model checking. In order to maximize the
reliability, one should deploy fault-tolerant distributed
algorithms that have been verified by model checking. However,
only very few distributed algorithms have been automatically
verified, because many aspects of distributed algorithms, such as
parameterization, faults, uncertain timing, etc. still pose
research challenges for model checking.

In this talk I will discuss several verification techniques that
we recently generalized and used for automatic verification of
distributed algorithms. These techniques include parametric
interval data and counter abstraction, offline partial order
reductions, and acceleration.

Based on joint work with Annu Gmeiner, Igor Konnov, Helmut Veith,
and Ulrich Schmid

Pour en savoir plus : https://parsys.lri.fr/seminar.html
Séminaires
A Two-level Auction for Resource Allocation in Mul
Réseaux sans fil et mobiles
Friday 09 March 2018 - 14h30
Salle : 445 - PCRI-N
Mira Morcos .............................................

Binary pattern of length greater than 14 are abeli
Combinatoire
Friday 09 February 2018 - 14h30
Salle : 445 - PCRI-N
Matthieu Rosenfeld .............................................

Approximate Bayesian Computation and Random Forest
Thursday 08 February 2018 - 00h00
Salle : 455 - PCRI-N
Valentin Thouzeau .............................................

A concurrent lock-free algorithm for computing a f
Combinatoire
Friday 12 January 2018 - 14h30
Salle : 445 - PCRI-N
James Mitchell .............................................

Acyclic Partitioning of Large Directed Acyclic Gra
Calcul à haute performance
Tuesday 09 January 2018 - 10h30
Salle : 465 - PCRI-N
Julien Herrmann .............................................