A Formalization of Powerlist Algebra in ACL2

被引:4
|
作者
Gamboa, Ruben A. [1 ]
机构
[1] Univ Wyoming, Dept Comp Sci, Laramie, WY 82071 USA
关键词
Powerlists; Verification; ACL2;
D O I
10.1007/s10817-009-9140-y
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
In Misra (ACM Trans Program Lang Syst 16(6):1737-1767, 1994), Misra introduced the powerlist data structure, which is well suited to express recursive, data-parallel algorithms. Moreover, Misra and other researchers have shown how powerlists can be used to prove the correctness of several algorithms. This success has encouraged some researchers to pursue automated proofs of theorems about powerlists (Kapur 1997; Kapur and Subramaniam 1995, Form Methods Syst Des 13(2):127-158, 1998). In this paper, we show how ACL2 can be used to verify theorems about powerlists. We depart from previous approaches in two significant ways. First, the powerlists we use are not the regular structures defined by Misra; that is, we do not require powerlists to be balanced trees. As we will see, this complicates some of the proofs, but on the other hand it allows us to state theorems that are otherwise beyond the language of powerlists. Second, we wish to prove the correctness of powerlist algorithms as much as possible within the logic of powerlists. Previous approaches have relied on intermediate lemmas which are unproven (indeed unstated) within the powerlist logic. However, we believe these lemmas must be formalized if the final theorems are to be used as a foundation for subsequent work, e.g., in the verification of system libraries. In our experience, some of these unproven lemmas presented the biggest obstacle to finding an automated proof. We illustrate our approach with two case studies involving Batcher sorting and prefix sums.
引用
收藏
页码:139 / 172
页数:34
相关论文
共 50 条
  • [1] A Formalization of Powerlist Algebra in ACL2
    Ruben A. Gamboa
    [J]. Journal of Automated Reasoning, 2009, 43 : 139 - 172
  • [2] Fourier Series Formalization in ACL2(r)
    Chau, Cuong K.
    Kaufmann, Matt
    Hunt, Warren A., Jr.
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (192): : 35 - 51
  • [3] The Fundamental Theorem of Algebra in ACL2
    Gamboa, Ruben
    Cowles, John
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (280): : 98 - 110
  • [4] ACL2
    Gamboa, R
    [J]. SEVENTEEN PROVERS OF THE WORLD, 2006, 3600 : 55 - 66
  • [5] Verified computer algebra in ACL2 (Grobner bases computation)
    Medina-Bulo, I
    Palomo-Lozano, F
    Alonso-Jiménez, JA
    Ruiz-Reina, JL
    [J]. ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION, PROCEEDINGS, 2004, 3249 : 171 - 184
  • [6] ACL2(ml): Machine-Learning for ACL2
    Heras, Jonathan
    Komendantskaya, Ekaterina
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (152): : 61 - 75
  • [7] ACL2
    [J]. Lect. Notes Comput. Sci., 2006, (55-66):
  • [8] Iteration in ACL2
    Kaufmann, Matt
    Moore, J. Strother
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2020, (327): : 16 - 31
  • [9] How Can I Do That with ACL2? Recent Enhancements to ACL2
    Kaufmann, Matt
    Moore, J. Strother
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (70): : 46 - 60
  • [10] An ACL2 tutorial
    Kaufmann, Matt
    Moore, J. Strother
    [J]. THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2008, 5170 : 17 - +