Abstract
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.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Boyer, R.S., Moore, J.S.: A Computational Logic. Academic, Orlando (1979)
Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic, San Diego (1988)
Brock, B., Kaufmann, M., Moore, J.S.: Rewriting with equivalence relations in ACL2. J. Autom. Reason. 40(4), 293–306 (2008)
Corman, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms, chap. 32. McGraw-Hill, New York (1990)
Greve, D.: Parameterized congruences in ACL2. In: Proceedings of the Sixth International Workshop of the ACL2 Theorem Prover and its Applications (ACL2-2006) (2006)
Kapur, D.: Constructors can be partial too. In: Veroff, R. (ed.) Automated Reasoning and Its Applications: Essays in Honor of Larry Wos. MIT, Cambridge (1997)
Kapur, D., Subramaniam, M.: Automated reasoning about parallel algorithms using powerlists. Technical Report TR-95-14, State University of New York at Albany (1995)
Kapur, D., Subramaniam, M.: Mechanical verification of adder circuits using rewrite rulelaboratory. Form. Methods Syst. Des. 13(2), 127–158 (1998)
Kaufmann, M., Moore, J.S.: The ACL2 home page. http://www.cs.utexas.edu/users/moore/acl2/acl2-doc.html
Kaufmann, M., Moore, J.S.: Design goals for ACL2. Technical Report 101, Computational Logic, Inc. http://www.cs.utexas.edu/-users/moore/publications/acl2-papers.html#Overviews (1994)
Kaufmann, M., Moore, J.S.: An industrial strength theorem prover for a logic based on common lisp. IEEE Trans. Softw. Eng. 23(4), 203–213 (1997)
Kornerup, J.: Odd-even sort in powerlists. Inf. Process. Lett. 61(1), 15–24 (1997)
Kornerup, J.: Parlists: a generalization of powerlists. In: Proceedings of Euro-Par’97 (1997)
Misra, J.: Powerlists: a structure for parallel recursion. ACM Trans. Program. Lang. Syst. 16(6), 1737–1767 (1994)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Gamboa, R.A. A Formalization of Powerlist Algebra in ACL2. J Autom Reasoning 43, 139–172 (2009). https://doi.org/10.1007/s10817-009-9140-y
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-009-9140-y