Generating and Exploiting Automated Reasoning Proof Certificates: 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. - BARBOSA, HANIEL; BARRETT, CLARK; COOK, BYRON; DUTERTRE, BRUNO; KREMER, GEREON; LACHNITT, HANNA; NIEMETZ, AINA; NÖTZLI, ANDRES; OZDEMIR, ALEX; PREINER, MATHIAS; REYNOLDS, ANDREW; TINELLI, CESARE; et al. (Communications of the ACM, 2023)
The article discusses various aspects of automated reasoning proof certificates, and it mentions the use of automated reasoning tools to find computer hardware and software-related bugs and security vulnerabilities. According to the article, formal proof certificates help improve trustworthiness. Satisfiability Modulo Theories (SMT), the efficient production of proofs, and SMT solvers are also assessed.