Generating and Exploiting Automated Reasoning Proof Certificates

“Generating and Exploiting Automated Reasoning Proof Certificates” by Haniel Barbosa, Clark Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, and Yoni Zohar. Communications of the Association for Computing Machinery (CACM), vol. 66, no. 10, Oct. 2023, pp. 86-95, Association for Computing Machinery.

Abstract

Moving toward a full suite of proof-producing automated reasoning tools with SMT solvers that can produce full, independently checkable proofs for real-world problems.

BibTeX entry:

@article{BBC+23,
   author = {Haniel Barbosa and Clark Barrett and Byron Cook and Bruno
	Dutertre and Gereon Kremer and Hanna Lachnitt and Aina Niemetz and
	Andres N{\"o}tzli and Alex Ozdemir and Mathias Preiner and Andrew
	Reynolds and Cesare Tinelli and Yoni Zohar},
   title = {Generating and Exploiting Automated Reasoning Proof Certificates},
   journal = {Communications of the Association for Computing Machinery
	(CACM)},
   volume = {66},
   number = {10},
   pages = {86--95},
   publisher = {Association for Computing Machinery},
   month = oct,
   year = {2023},
   doi = {10.1145/3587692},
   url = {http://dx.doi.org/10.1145/3587692}
}

(This webpage was created with bibtex2web.)