Sciweavers

IPPS
1998
IEEE

Mechanically Verifying the Correctness of the Fast Fourier Transform in ACL2

14 years 3 months ago
Mechanically Verifying the Correctness of the Fast Fourier Transform in ACL2
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.
Ruben Gamboa
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where IPPS
Authors Ruben Gamboa
Comments (0)