Abstract
In [10], Misra introduced the powerlist data structure, which is well suited to express recursive, data-parallel algorithms. In particular, Misra showed how powerlists could be used to give simple descriptions to very complex algorithms, such as the Fast Fourier Transform (FFT). Such simplicity in presentation facilitates reasoning about the resulting algorithms, and in fact Misra was able to give a stunningly simple proof of the correctness of the FFT. In this paper, we show how this proof can be verified using ACL2. This strengthens Misra's case that powerlists provide a suitable framework in which to define and reason about parallel algorithms, particularly using mechanical tools to aid in reasoning.
Work was performed while author was a student at the University of Texas at Austin.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Brock, B., Kaufmann, M., Moore, J: Ac12 theorems about commercial microprocessors. Formal Methods in Computer-Aided Design (FMCAD'96). (1996) 275–293.
Boyer, R., Moore, J: A Computational Logic. Academic Press. Orlando. (1979)
Boyer, R., Moore, J: A Computational Logic Handbook. Academic Press. San Diego. (1988)
Corman, T., Leiserson, C., Rivest, R.: Introduction to Algorithms, chapter 32. McGraw-Hill. New York. (1990)
Gamboa, R.: Defthms about zip and tie: Reasoning about powerlists in ACL2. Univ. of Texas Comp. Sci. Tech. Rep. TR97-02. (1997)
Kaufmann, M., Moore J: ACL2 Version 1.9 Documentation. Computational Logic, Inc.
Kaufmann, M., Moore J: Design goals for ACL2. Computational Logic, Inc. Tech. Rep. 101. (1994)
Kaufmann, M., Moore J: An industrial strength theorem prover for a logic based on common lisp. IEEE Transactions on Software Engineering. 23(4) (1997) 203–213
Kaufmann, M., Pecchiari, P.: Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem. Computational Logic, Inc. Tech. Rep. 100. (1994)
Misra, J.: Powerlists: A structure for parallel recursion. ACM Trans. on Prog. Lang. and Systems. 16(6) (1994) 1737–1767
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gamboa, R.A. (1998). Mechanically verifying the correctness of the Fast Fourier Transform in ACL2. In: Rolim, J. (eds) Parallel and Distributed Processing. IPPS 1998. Lecture Notes in Computer Science, vol 1388. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-64359-1_743
Download citation
DOI: https://doi.org/10.1007/3-540-64359-1_743
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64359-3
Online ISBN: 978-3-540-69756-5
eBook Packages: Springer Book Archive