Semenov, Alexander; Otpuschennikov, Ilya; Gribanova, Irina; Zaikin, Oleg; Kochemazov, Stepan Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems. (English) Zbl 07199588 Log. Methods Comput. Sci. 16, No. 1, Paper No. 29, 42 p. (2020). MSC: 03B70 68 PDF BibTeX XML Cite \textit{A. Semenov} et al., Log. Methods Comput. Sci. 16, No. 1, Paper No. 29, 42 p. (2020; Zbl 07199588) Full Text: Link arXiv
Marić, Filip Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points. (English) Zbl 07038739 J. Autom. Reasoning 62, No. 3, 301-329 (2019). MSC: 68T15 PDF BibTeX XML Cite \textit{F. Marić}, J. Autom. Reasoning 62, No. 3, 301--329 (2019; Zbl 07038739) Full Text: DOI
Philipp, Tobias An expressive model for instance decomposition based parallel SAT solvers. (English) Zbl 06688810 Lutz, Carsten (ed.) et al., Frontiers of combining systems. 10th international symposium, FroCoS 2015, Wrocław, Poland, September 21–24, 2015. Proceedings. Cham: Springer (ISBN 978-3-319-24245-3/pbk; 978-3-319-24246-0/ebook). Lecture Notes in Computer Science 9322. Lecture Notes in Artificial Intelligence, 101-116 (2015). MSC: 68T PDF BibTeX XML Cite \textit{T. Philipp}, Lect. Notes Comput. Sci. 9322, 101--116 (2015; Zbl 06688810) Full Text: DOI
Davis, Jared; Myreen, Magnus O. The reflective Milawa theorem prover is sound (down to the machine code that runs it). (English) Zbl 1356.68186 J. Autom. Reasoning 55, No. 2, 117-183 (2015). MSC: 68T15 PDF BibTeX XML Cite \textit{J. Davis} and \textit{M. O. Myreen}, J. Autom. Reasoning 55, No. 2, 117--183 (2015; Zbl 1356.68186) Full Text: DOI
Hidalgo-Doblado, M. J.; Alonso-Jiménez, J. A.; Borrego-Díaz, J.; Martín-Mateos, F. J.; Ruiz-Reina, J. L. Formally verified tableau-based reasoners for a description logic. (English) Zbl 1314.68282 J. Autom. Reasoning 52, No. 3, 331-360 (2014). MSC: 68T15 68Q60 68T27 PDF BibTeX XML Cite \textit{M. J. Hidalgo-Doblado} et al., J. Autom. Reasoning 52, No. 3, 331--360 (2014; Zbl 1314.68282) Full Text: DOI
Shankar, Natarajan; Vaucher, Marc The mechanical verification of a DPLL-based satisfiability solver. (English) Zbl 1347.68307 Haeusler, Edward Hermann (ed.) et al., Proceedings of the 5th workshop on logical and semantic frameworks, with applications (LSFA 2010), Natal, Brazil, August 31, 2010. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 269, 3-17 (2011). MSC: 68T15 68Q60 68T20 PDF BibTeX XML Cite \textit{N. Shankar} and \textit{M. Vaucher}, Electron. Notes Theor. Comput. Sci. 269, 3--17 (2011; Zbl 1347.68307) Full Text: DOI
Marić, Filip Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL. (English) Zbl 1208.68205 Theor. Comput. Sci. 411, No. 50, 4333-4356 (2010). MSC: 68T20 68Q60 PDF BibTeX XML Cite \textit{F. Marić}, Theor. Comput. Sci. 411, No. 50, 4333--4356 (2010; Zbl 1208.68205) Full Text: DOI