Model Checking Using Logic Solvers
le 7 février 2024
13h15Campus 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.
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