Skip to Main content Skip to Navigation
Conference papers

Verification of Faust Signal Processing Programs in COQ

Abstract : We report on our ongoing work to formalize and prove properties of FAUST programs using COQ. FAUST (Functional Audio Stream) is a functional programming language specifically designed for real-time digital signal processing (DSP) and synthesis. This Domain-Specific Language targets high-performance audio DSP applications and plug-ins for a variety of platforms and standards. Faust programs are highly declarative and provide a reasonable set of static guarantees, but far from full correctness. In FAUST's domain, when errors occur, one will typically experience problems by hearing audio glitches or, even worse, by suffering imperceptible distortion, which can accumulate and become audible when more components are connected. To detect such cases a priori, manual reasoning is far from trivial: arithmetic errors, feedback loops, and the large size of the DSP circuits involved make it tedious and error-prone. Thus, automated verification is highly desirable in the growing ecosystem of FAUST users and libraries. We intend to use COQ as the basis for a specification and automated verification platform for FAUST programs. We plan to use the resulting tool to certify library components, as well as to experiment with new language features or to enhance the FaustWorks IDE with proof automation features. Our choice of COQ instead of a custom-purpose tool is both pragmatic and philosophical: we believe that we can greatly profit from the existing tools and libraries, and that others may do so too from our effort. The anticipated two main challenges: useful and modular au-tomation, and integration of a quite diverse set of existing libraries.
Document type :
Conference papers
Complete list of metadatas

https://hal-mines-paristech.archives-ouvertes.fr/hal-01108173
Contributor : Claire Medrala <>
Submitted on : Thursday, January 22, 2015 - 2:38:10 PM
Last modification on : Wednesday, October 14, 2020 - 3:52:19 AM
Long-term archiving on: : Thursday, April 23, 2015 - 10:30:58 AM

File

A-593.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01108173, version 1

Citation

Emilio Jesús Gallego Arias, Olivier Hermant, Pierre Jouvelot. Verification of Faust Signal Processing Programs in COQ. The 1st International Workshop on Coq for PL (Co-located with POPL), Jan 2015, Mumbai, India. ⟨hal-01108173⟩

Share

Metrics

Record views

461

Files downloads

89