Verification of Faust Signal Processing Programs in COQ
Résumé
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.
Origine : Fichiers produits par l'(les) auteur(s)