user

Advances in ACL2 Proof Debugging Tools*

被引：0
|
作者：
Kaufmann, Matt [1 ]
Moore, J. Strother [1 ]
机构：
[1] Univ Texas Austin, Dept Comp Sci, Austin, TX 78712 USA
来源：
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2023年 / 393卷
关键词：
D O I：
10.4204/EPTCS.393.7
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
The experience of an ACL2 user generally includes many failed proof attempts. A key to successful use of the ACL2 prover is the effective use of tools to debug those failures. We focus on changes made after ACL2 Version 8.5: the improved break-rewrite utility and the new utility, with-brr-data.
引用
收藏
页码：67 / 81
页数：15
相关论文
共 50 条
  • [1] Integrating external deduction tools with ACL2
    Kaufmann, Matt
    Moore, J. Strother
    Ray, Sandip
    Reeber, Erik
    [J]. JOURNAL OF APPLIED LOGIC, 2009, 7 (01) : 3 - 25
  • [2] Proof Pearl: a Formal Proof of Higman's Lemma in ACL2
    Jesus Martin-Mateos, Francisco
    Luis Ruiz-Reina, Jose
    Antonio Alonso, Jose
    Jose Hidalgo, Maria
    [J]. JOURNAL OF AUTOMATED REASONING, 2011, 47 (03) : 229 - 250
  • [3] Proof pearl:: A formal proof of Higman's lemma in ACL2
    Martín-Mateos, FJ
    Ruiz-Reina, JL
    Alonso, JA
    Hidalgo, MJ
    [J]. THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2005, 3603 : 358 - 372
  • [4] A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2
    Coglio, Alessandro
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2022, (359): : 185 - 201
  • [5] An ACL2 proof of write invalidate cache coherence
    Moore, JS
    [J]. COMPUTER AIDED VERIFICATION, 1998, 1427 : 29 - 38
  • [6] A formal proof of Dickson's Lemma in ACL2
    Martín-Mateos, FJ
    Alonso, JA
    Hidalgo, MJ
    Ruiz-Reina, JL
    [J]. LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2003, 2850 : 49 - 58
  • [7] Proof Pad: A New Development Environment for ACL2
    Eggensperger, Caleb
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (114): : 13 - 28
  • [8] Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2
    Francisco Jesús Martín-Mateos
    José Luis Ruiz-Reina
    José Antonio Alonso
    María José Hidalgo
    [J]. Journal of Automated Reasoning, 2011, 47 : 229 - 250
  • [9] ACL2
    Gamboa, R
    [J]. SEVENTEEN PROVERS OF THE WORLD, 2006, 3600 : 55 - 66
  • [10] The correctness of the fast Fourier transform: A structured proof in ACL2
    Gamboa, RA
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2002, 20 (01) : 91 - 106
12345