+++
title = "SMTCoq as a formalisation in Coq"
date = "2022-08-02"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3d2a"]
forwardlinks = ["3d2b1"]
zettelid = "3d2b"
+++

SMTCoq \[1\] is a tool that formalises these rewriting traces in Coq, so
that traces from various tools (veriT, cvc4 and zchaff) can be read and
then checked according to the input formula. This actually does not
require any trust in the parsing and pretty printing to pass the input
to the SAT solver, because the initial formula is already represented in
Coq, then the trace will also be represented in Coq, and so the checker
can just check that this arbitrary trace present in Coq does indeed
simplify the formula to $\perp$.

<div id="refs" class="references csl-bib-body" markdown="1">

<div id="ref-armand11_modul_integ_sat_smt_solver" class="csl-entry"
markdown="1">

<span class="csl-left-margin">\[1\]
</span><span class="csl-right-inline">M. Armand, G. Faure, B. Grégoire,
C. Keller, L. Théry, and B. Werner, “A modular integration of SAT/SMT
solvers to coq through proof witnesses,” in *Certified programs and
proofs*, J.-P. Jouannaud and Z. Shao, Eds., Berlin, Heidelberg: Springer
Berlin Heidelberg, 2011, pp. 135–150. doi:
[10.1007/978-3-642-25379-9_12].</span>

</div>

</div>

  [10.1007/978-3-642-25379-9_12]: https://doi.org/10.1007/978-3-642-25379-9_12