Evènement pour le groupe Modélisation et Verification


Date 2013-10-17  11:00-12:00
TitreSAT Solvers and Model Checking 
RésuméSince the first complete SAT solvers (DPLL-62, based on classical backtrack-search), major breakthroughs were observed in the practical – and theoretical – study of SAT. Nowadays, SAT solvers can be used in many critical systems, from very hard problems (Formal Verification, Biology, Cryptology) with potentially long runs, to more reactive applications (were a SAT solver can be called many times per second). In this talk, we will review the progresses made since the first breakthrough of 2001, with the introduction of CDCL solvers, called “modern solvers”. We will show how the field is slowly moving from a “complete” vision of Solvers to a more “uncomplete” one. We will end the talk by some open questions on the future of SAT Solvers, and the recent trends in "incremental SAT Solving", where SAT solvers are called thousand times for each run. 
Lieu076 
OrateurLaurent Simon 
Emaillsimon@labri.fr 
UrlLaBRI 



Aucun document lié à cet événement.

Retour
Retour à l'index