Extending Coq with Imperative Features and Its Application to SAT Verification. - Michaël Armand; Benjamin Grégoire; Arnaud Spiwack; Laurent Théry (ITP, 2010)

A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. - Michaël Armand; Germain Faure; Benjamin Grégoire; Chantal Keller; Laurent Théry; Benjamin Werner (CPP, 2011)