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.
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. Sa...
| Publicado en: | Communications of the ACM Vol. 66; no. 10; pp. 86 - 96 |
|---|---|
| Autores principales: | , , , , , , , , , , , , |
| Formato: | Artículo |
| Publicado: |
Association for Computing Machinery
Oct2023
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=172339329&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 172339329 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Oct2023 vid: 66 iid: 10 pid: 68 pub: Association for Computing Machinery artinfo: ui: 172339329 10.1145/3587692 ppf: 86 ppct: 10 formats: tig: atl: 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. aug: au: 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 affil: Universidade Federal de Minas Gerais, Belo Horizonte, Brazil Stanford University, Stanford, CA, USA Amazon, New York, NY, USA and University College London, UK Amazon, New York, NY, USA The University of Iowa, Iowa City, USA Bar-Ilan University, Ramat Gan, Israel su: Reasoning Automation Debugging Computer security vulnerabilities Satisfiability (Computer science) Trust sug: subj: Reasoning Automation Debugging Computer security vulnerabilities Satisfiability (Computer science) Trust ab: 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. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2023 holdings: @attributes: islocal: N |
|---|