Verification of Algorithm and Code Generation for Signal Transforms
This extended abstract presents a the formally verification a subset of SPIRAL, an efficient code generation system for digital signal processing algorithms and related computations. SPIRAL represents algorithms for linear transforms as sparse matrix factorizations using a domain specific language called the Signal Processing Language (SPL). To produce an algorithm, SPL expressions representing a signal transform factorization are rewritten through repeated application of factorization and matrix identities. SPL expressions representing completely factorized transforms can be compiled to a target language. A subset of SPIRAL’s algorithm space as well as an SPL compiler targeting a simple imperative language with arrays and values from a commutative ring, IMP+V, are verified using the Coq proof assistant.
Tue 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:00 - 18:45
|Verification of Algorithm and Code Generation for Signal Transforms|
|An experience report on writing usable DSLs in Coq|