3 ms·
With a proof checker. They're usually tiny for easier verification. Some are trying to verify the verifiers. HOL/Light and Jared Davis's Milawa esp come to mind
by nickpsecurity 9y ago
With a proof checker. They're usually tiny for easier verification. Some are trying to verify the verifiers. HOL/Light and Jared Davis's Milawa esp come to mind. Milawa's layered approach is pretty neat.
http://www.cs.utexas.edu/users/jared/milawa/Web/ http://www.cs.utexas.edu/users/jared/milawa/Web/
- rrobukef 9y agoThere is a verified DRAT-trim (the proof checking format used) implementation in Isabelle/HOL [1]. Apparently it is faster than the original: ``We have presented a formally verified tool chain to check DRAT unsatisfiability certificates. In single-threaded mode, our approach is more than two times faster than the (unverified) standard tool drat-trim, on a benchmark suite taken from the 2016 SAT competition.'' [1] Lammich, Peter. "Efficient verified (UN) SAT certificate checking." International Conference on Automated Deduction. Springer, Cham, 2017.
- nickpsecurity 9y agoNeat. Here's two more on that topic that go further: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.459.7149 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.459.... http://matryoshka.gforge.inria.fr/pubs/sat_sister.pdf http://matryoshka.gforge.inria.fr/pubs/sat_sister.pdf