[Matryoshka-devel] One more Draft --- A Verified SAT Solver with Two Watched Literals Using Imperative HOL
mathias.fleury at mpi-inf.mpg.de
Wed Apr 12 16:17:41 CEST 2017
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
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 842 bytes
Desc: OpenPGP digital signature
More information about the matryoshka-devel