Bit-Blasting ACL2 Theorems

被引：19
|
作者：
Swords, Sol [1 ]
Davis, Jared [1 ]
机构：
[1] Centaur Technol Inc, 7600-C N Capital Texas Hwy,Suite 300, Austin, TX 78731 USA
来源：
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2011年 / 70期
关键词：
D O I：
10.4204/EPTCS.70.7
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Interactive theorem proving requires a lot of human guidance. Proving a property involves (1) figuring out why it holds, then (2) coaxing the theorem prover into believing it. Both steps can take a long time. We explain how to use GL, a framework for proving finite ACL2 theorems with BDD-or SAT-based reasoning. This approach makes it unnecessary to deeply understand why a property is true, and automates the process of admitting it as a theorem. We use GL at Centaur Technology to verify execution units for x86 integer, MMX, SSE, and floating-point arithmetic.
引用
收藏
页码：84 / 102
页数：19
相关论文
共 50 条
  • [1] Scalable Bit-Blasting with Abstractions
    Niemetz, Aina
    Preiner, Mathias
    Zohar, Yoni
    [J]. COMPUTER AIDED VERIFICATION, PT I, CAV 2024, 2024, 14681 : 178 - 200
  • [2] ACL2 theorems about commercial microprocessors
    Brock, B
    Kaufmann, M
    Moore, JS
    [J]. FORMAL METHODS IN COMPUTER-AIDED DESIGN, 1996, 1166 : 275 - 293
  • [3] Improving Bit-Blasting for Nonlinear Integer Constraints
    Jia, Fuqi
    Han, Rui
    Huang, Pei
    Liu, Minghao
    Ma, Feifei
    Zhang, Jian
    [J]. PROCEEDINGS OF THE 32ND ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON SOFTWARE TESTING AND ANALYSIS, ISSTA 2023, 2023, : 14 - 25
  • [4] Second-Order Functions and Theorems in ACL2
    Coglio, Alessandro
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (192): : 17 - 33
  • [5] Term-Level Reasoning in Support of Bit-blasting
    Swords, Sol
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (249): : 95 - 111
  • [6] Proving theorems about Java']Java and the JVM with ACL2
    Moore, JS
    [J]. MODELS, ALGEBRAS AND LOGIC OF ENGINEERING SOFTWARE, 2003, 191 : 227 - 290
  • [7] ACL2
    Gamboa, R
    [J]. SEVENTEEN PROVERS OF THE WORLD, 2006, 3600 : 55 - 66
  • [8] ACL2(ml): Machine-Learning for ACL2
    Heras, Jonathan
    Komendantskaya, Ekaterina
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (152): : 61 - 75
  • [9] ACL2
    [J]. Lect. Notes Comput. Sci., 2006, (55-66):
  • [10] Building Better Bit-Blasting for Floating-Point Problems
    Brain, Martin
    Schanda, Florian
    Sun, Youcheng
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, 2019, 11427 : 79 - 98
12345