Abstract
The powerlists data structure, created by Misra in the early 90s, is well suited to express recursive, data-parallel algorithms. Misra has shown how powerlists can 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 has presented a stunningly simple proof of the correctness of the FFT. In this paper, we show how this proof can be mechanically verified using the ACL2 theorem prover. This supports Misra's belief that powerlists provide a suitable framework in which to define and reason about parallel algorithms, particularly using mechanical tools. It also illustrates the use of ACL2 in the formal verification of a distributed algorithm.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
R. Boyer and J. Moore, A Computational Logic, Academic Press, Orlando, 1979.
R. Boyer and J. Moore, A Computational Logic Handbook, Academic Press, San Diego, 1988.
B. Brock, M. Kaufmann, and J. Moore, “ACL2 theorems about commercial microprocessors,” in Formal Methods in Computer-Aided Design (FMCAD'96), 1996, pp. 275-293.
R. Churchill and J. Brown, Complex Variables and Applications, McGraw-Hill, New York, 1984.
T. Corman, C. Leiserson, and R. Rivest, Introduction to Algorithms, McGraw-Hill, New York, Ch. 32, 1990.
R. Gamboa, “Defthms about zip and tie: Reasoning about powerlists in ACL2,” University of Texas Comp. Sci., Technical Report TR97-02, 1997.
D. Kapur, “Constructors can be partial, too,” in R. Veroff et al. (Ed.), Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1997.
D. Kapur and M. Subramaniam, “Automated reasoning about parallel algorithms using powerlists,” State University of New York at Albany, Technical Report TR-95-14, 1995.
D. Kapur and H. Zhang, “An overview of Rewrite Rule Laboratory (RRL),” Journal of Computer and Mathematics with Applications, 1995.
M. Kaufmann, “ACL2 support for verification projects,” in Proc. 15th Intl. Conf. on Automated Deduction, 1998, pp. 220-238.
M. Kaufmann and J. Moore, “ACL2: A computational logic for applicative common lisp, the user's manual,” available in the world-wide web at http://www.cs.utexas.edu/users/moore/acl2.
M. Kaufmann, P. Manolios, and J. Moore, Computer-Aided Reasoning: An Approach, Kluwer Academic Press, 2000.
M. Kaufmann and J. Moore, “An industrial strength theorem prover for a logic based on common lisp,” IEEE Transactions on Software Engineering, Vol. 23, No. 4, pp. 203-213, 1997.
M. Kaufmann and J. Moore, “Structured theory development for a mechanized logic,” Journal of Automated Reasoning, 2001.
M. Kaufmann and P. Pecchiari, “Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem,” Computational Logic, Inc., Technical Report 100, 1994.
J. Misra, “Powerlists: A structure for parallel recursion,” ACM Trans. on Prog. Lang. and Systems, Vol. 16, No. 6, pp. 1737-1767, 1994.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Gamboa, R.A. The Correctness of the Fast Fourier Transform: A Structured Proof in ACL2. Formal Methods in System Design 20, 91–106 (2002). https://doi.org/10.1023/A:1012912614285
Issue Date:
DOI: https://doi.org/10.1023/A:1012912614285