Logo IRISA logo Inria

Prochains Exposés

jeudi 27 avril, 14h en salle Markov

Josef Widder

Model Checking Fault-tolerant Distributed Algorithms

Distributed algorithms have numerous mission-critical applications in embedded avionic and automotive systems, cloud computing, computer networks, hardware design, and the internet of things. Although distributed algorithms exhibit complex interactions with their computing environment and are difficult to understand for human engineers, computer science has developed only very limited tool support to catch logical errors in distributed algorithms at design time. In the last two decades we have witnessed a revolutionary progress in software model checking due to the development of powerful techniques such as abstract model checking, SMT solving, and partial order reduction. Still, model checking of fault-tolerant distributed algorithms poses multiple research challenges, most notably parameterized verification: verifying an algorithm for all system sizes and different combinations of faults. I will present our recent results in this area which extend and combine abstraction, partial orders, and bounded model checking. Our results demonstrate that model checking has acquired sufficient critical mass to build the theory and the practical tools for the formal verification of fault-tolerant distributed algorithms. Joint work with Igor Konnov, Marijana Lazic, and Helmut Veith

Exposés des semaines suivantes

jeudi 18 mai, 14h en salle Aurigny

Simon Lunel

Compositional proofs in differential dynamic logic

Modularity and composability are essential properties to facilitate and scale the design of cyber-physical systems from the specification of hybrid, discrete and continuous, components. Modularity is essential to break down a system model into comprehensible and manageable component specifications. Composability is essential to design a system from component models while preserving their verified properties, expressed as assume-guarantee contracts. I will present our recent results which address the specification of hybrid system using Platzer's differential dynamic logic. We define a new composition operator in differential dynamic logic and prove that it is associative and commutative. Plus, we provide a theorem which characterizes necessary conditions to automate the proof that composed components satisfy the composition of their individual contracts, enabling modular and compositional verification. We case-study our composition operator by considering the modular and detailed specification of a cruise controller in KeYmaera X. (Joint work with Jean-Pierre Talpin and Benoit Boyer)

jeudi 8 juin, 14h en salle Aurigny

Loïc Hélouët

To be announced

To Be announced

jeudi 15 juin, 14h en salle Aurigny

Béatrice Bérard

To be announced

To Be announced

Séminaire autour des thèmes 68NQRT