[Matryoshka-devel] Paper draft: A Verified SAT Solver with Watched Literals Using Imperative HOL

Mathias Fleury mathias.fleury at mpi-inf.mpg.de
Wed Oct 25 15:19:58 CEST 2017


Dear colleagues,


I would like to share the draft of the paper we have submitted to CPP:

A Verified SAT Solver with Watched Literals Using Imperative HOL
Jasmin Christian Blanchette, Mathias Fleury, and Peter Lammich

http://matryoshka.gforge.inria.fr/pubs/sat_2wl_paper.pdf <http://matryoshka.gforge.inria.fr/pubs/sat_2wl_paper.pdf>


The paper is about the refinement from the CDCL calculus in Isabelle to a calculus that includes two watched literals. After that, we refine this calculus to deterministic correct code that can be exported to imperative code. By connecting it to an unverified parser, we obtain a SAT solver in Standard ML called IsaSAT.


Feedback is welcome.

Mathias
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/matryoshka-devel/attachments/20171025/23d56b8d/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 874 bytes
Desc: Message signed with OpenPGP
URL: <http://lists.gforge.inria.fr/pipermail/matryoshka-devel/attachments/20171025/23d56b8d/attachment.sig>


More information about the matryoshka-devel mailing list