A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses.

Michal Armand, Germain Faure, Benjamin Grgoire, Chantal Keller, Laurent Thry, Benjamin Werner

Browse the full CPP paper archive.