[Matryoshka-devel] One more Draft --- A Verified SAT Solver with Two Watched Literals Using Imperative HOL

Mathias Fleury mathias.fleury at mpi-inf.mpg.de
Wed Apr 12 16:17:41 CEST 2017


Dear colleagues,

Here is the most recent draft of the paper that we will submit to ITP.

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

	http://people.mpi-inf.mpg.de/~mfleury/sat_twl.pdf

The article presents the refinement to imperative ML code, using Imperative HOL and the Refinement Framework, and presents the two-watched-literal data structure. We will submit the paper on Thursday afternoon but will also accept feedback afterwards. It expands on the refinement part of our recent JAR submission.


Best regards,
Mathias 



-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 842 bytes
Desc: OpenPGP digital signature
URL: <http://lists.gforge.inria.fr/pipermail/matryoshka-devel/attachments/20170412/dfab2a3a/attachment.sig>


More information about the matryoshka-devel mailing list