Mercredi 30/06/2010, à partir de 11h, en salle Byron Blanc.
Orateur : Michaël Armand.
Titre : De SAT à SMT.
Résumé :
Pour ceux qui n’y ont pas encore eu droit, je vous montrerais comment on utilise un solveur SAT pour construire un solveur SMT : Satisfiability Modulo Theories. J’illustrerais le principe avec une théorie particulière (EUF soit Equality with Uninterpreted Functions), et je montrerais comment combiner plusieurs théories pour en arriver à un solveur SMT performant. Enfin, j’expliquerais comment faire on peut faire croire ça à Coq!
