Verification of Algorithm and Code Generation for Signal Transforms
summary
A formalization verifies a nontrivial subset of SPIRAL: SPL rewrite rules are proven to preserve matrix semantics and a Coulee–Tukey factorization is proved by evaluation on standard basis vectors. A compiler from SPL to a simple imperative language with arrays and ring values is implemented and verified in Coq proofs, with code templates checked using Hoare logic and a mechanized semantics library for total correctness including termination. No C backend or floating point guarantees yet; vectorization is future work.
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
23mGenerating Programs for Polynomial Multiplication with Correctness Assurance
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
01h 06mVerifying a compiler through equational means