التفاصيل البيبلوغرافية
| العنوان: |
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, ZOHAR, YONI |
| المصدر: |
Communications of the ACM; Oct2023, Vol. 66 Issue 10, p86-95, 10p, 1 Color Photograph, 1 Black and White Photograph, 2 Diagrams |
| مصطلحات موضوعية: |
REASONING, AUTOMATION, DEBUGGING, COMPUTER security vulnerabilities, SATISFIABILITY (Computer science), TRUST |
| مستخلص: |
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. |
| قاعدة البيانات: |
Complementary Index |
