Verification of Algorithm and Code Generation for Signal Transforms
summary
Coq-verified subset of SPIRAL formalizes SPL matrix semantics and proves rewrite rules preserve matrices (including a mechanized Cooley–Tukey factorization using primitive roots of unity over commutative rings). A compiler from SPL to a simple imperative language IMP+V is proved correct with Hoare-style, total correctness proofs (termination included) and fresh-name handling for temporaries. Current scope targets algebraic transforms and array code; C generation, floating-point error bounds and vectorization/parallelization remain unverified and in progress.
AI-written summary · about
chapters (8)
- 0:00Intro
- 0:18Overview
- 0:35SPIRAL
- 2:44Algorithm Generation
- 5:08Correctness
- 6:09Supporting Mathematics
- 8:50Compilation to IMP+V
- 10:45Future Work
related talks
14mVerification of Algorithm and Code Generation for Signal Transforms
11mSemantics Lifting for Scientific Kernels
17mTowards Semantics Lifting for Scientific Computing: A Case Study on FFT
36mTowards a Formally-verified Software Toolchain for open ISAs
46mMechanizing Abstract Interpretation
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
30mAnalyzing Programs with SMT Solvers
19mAutomated Verification of Fundamental Algebraic Laws