How to certify a SAT-solver in a few lines of Coq ?
A Tutorial on Defensive Certification

Author Sylvain Boulmé

Description

Defensive Certification is a paradigm to produce formally certified software through defensive programming: this allows to reduce the certification effort to a small part of the software. The main difference with other skeptical methods like Proof carrying code or like Coq reflexive tactics is that the untrusted oracle and the skeptical verifier can communicate through a bi-directional API. Here, I link certified code in Coq to untrusted Ocaml code through Coq extraction.

This paper (submitted to VSTTE 2016) illustrates that defensive certification allows to develop a certified refutation prover for CNF, by focusing most of the development effort on an untrusted SAT-solver. Indeed, the certified part is both simple and tiny: only 30 Coq lines for the specification and around 200 Coq lines for the implementation (proof scripts included) -- all developed in one man.day. The current untrusted oracle is about 800 Ocaml lines developed in 1.5 man.month. But it does not yet implement all the optimizations of state-of-the-art SAT-solvers. The resulting prover is however already reasonably efficient (but not yet competitive with state-of-the-art SAT-solvers).

In conclusion, defensive certification seems to offer an interesting trade-off between the certification effort and the efficiency of the software. See the paper for more details.

Source code

You may download the source code in this archive. See file README in the archive for compilation details. The contents of the source archive is licensed under LGPL-2.1 (see file LICENSE in the archive).


Last modification: April 2016