diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-05-11 19:38:03 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-11 19:38:03 +0100 |
commit | 47c1289ff658a5aec71635d79ffe30bb29a07876 (patch) | |
tree | 56cf6b959e37fed88c492d34defd3d7ec40e7148 /content/zettel/3d2b.md | |
parent | fbe0fc62120348f582dc4db2b614078943d0764b (diff) | |
download | zk-web-47c1289ff658a5aec71635d79ffe30bb29a07876.tar.gz zk-web-47c1289ff658a5aec71635d79ffe30bb29a07876.zip |
Add content
Diffstat (limited to 'content/zettel/3d2b.md')
-rw-r--r-- | content/zettel/3d2b.md | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/content/zettel/3d2b.md b/content/zettel/3d2b.md new file mode 100644 index 0000000..f4898aa --- /dev/null +++ b/content/zettel/3d2b.md @@ -0,0 +1,38 @@ ++++ +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 |