Who Verifies the Verifiers? A Computer-Checked Implementation of the DPLL Algorithm in Dafny
The work
| Authors | Cezar-Constantin Andrici; Ştefan Ciobâcă |
|---|---|
| Editors | |
| Type | misc |
| Year | 2020 |
| Citekey | andrici2020who |
Identifiers
| arXiv | 2007.10842 from its landing_page_url |
|---|
Access
| Landing page | https://arxiv.org/abs/2007.10842 |
|---|
Related
| Distinct from | nukala2024translating |
|---|---|
| Supersedes | andrici2019verifying |
From bibtex.
Abstract
We build a SAT solver implementing the DPLL algorithm in the verification-enabled programming language Dafny. The resulting solver is fully verified (soundness, completeness and termination are computer checked). We benchmark our Dafny solver and we show that it is just as efficient as an equivalent DPLL solver implemented in C# and roughly two times less efficient than an equivalent solver written in C++. We conclude that auto-active verification is a promising approach to increasing trust in SAT solvers, as it combines a good trade-off between execution speed and degree of trustworthiness of the final product.
A copy is held
pdf, 482.6 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-17 06:13 UTC |
| Approved by | a person 2026-09-17 16:58 UTC |
Filed under
Cite it as
@misc{andrici2020who,
title = {Who Verifies the Verifiers? A Computer-Checked Implementation of the DPLL Algorithm in Dafny},
author = {Cezar-Constantin Andrici and Ştefan Ciobâcă},
year = {2020},
}
This record lives at https://refs.drheap.org/andrici2020who/ and will keep doing so.