On Thursday 28/05/2009, at 10h, in room Euler Bleu.
Speaker: Michaël Armand.
Title: Integrating SAT solvers in Coq.
Abstract:
Michael Armand will present his work with Benjamin Gregoire and Laurent Thery about integrating SAT solvers in Coq using certificates from an external SAT solver and an internal checker. The talk will explain SAT solving algorithms, certificates for SAT, and correctness proofs for the checker (in its state of the art!).
