Partager cette page :

Model Checking Using Logic Solvers

le 7 février 2024

13h15

Campus de Beaulieu Salle i-50 - bât. 12D

Intervention de Ocan Sankur, chargé de recherche au CNRS dans l'équipe DEVINE, (anciennement SUMO) à l'IRISA, dans le cadre des séminaires du département Informatique.

/medias/photo/seminaire-di_1630676501273-jpg

We present algorithms for formally verifying Boolean systems, that is, programs that can be modeled using Boolean variables only. This setting is very useful for modeling hardware protocols, or even distributed algorithms. State-of-the-art algorithms for model checking often use logic solvers. Here, we will focus on the use of SAT solvers. I will present how systems can be modeled using propositional logic, and how such solvers can be used for efficient model checking.
Thématique(s)
Formation, Recherche - Valorisation
Contact
Killian Barrere

Mise à jour le 7 février 2024