Verification of Faust Signal Processing Programs in COQ - Mines Paris Accéder directement au contenu
Communication Dans Un Congrès Année : 2015

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.
Fichier principal
Vignette du fichier
A-593.pdf (101.11 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-01108173 , version 1 (22-01-2015)

Identifiants

  • HAL Id : hal-01108173 , version 1

Citer

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⟩
305 Consultations
67 Téléchargements

Partager

Gmail Facebook X LinkedIn More