Selected publications at LSV

The election of a leader in a network is a challenging task, especially when the processes are asynchronous, i.e., execute an algorithm with time-varying periods. Thales developed an industrial election algorithm with an arbitrary number of processes, that can possibly fail. In this work, we prove the correctness of a variant of this industrial algorithm. We use a method combining abstraction, the SafeProver solver, and a parametric timed model-checker. This allows us to prove the correctness of the algorithm for a large number p of processes (p = 5000).

   address = {Cascais/Lisbon, Portugal},
   author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Mota, Jean-Marc and Soulat, Romain},
   booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on {V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation ({VMCAI}'19)},
   editor = {Enea, Constantin and Piskac, Ruzica},
   month = jan,
   note = {To appear},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking},
   year = {2019},

About LSV

Select by Year