The Correctness of the Fast Fourier Transform: A Structured Proof in ACL2

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.

• Type: Journal
• Year: 2002
• Where: FMSD
• Authors: Ruben Gamboa
• Keywords: Algorithm, FMSD 2002, Misra, Powerlists Data Structure