Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

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.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal-mines-paristech.archives-ouvertes.fr/hal-01108173
Contributeur : Claire Medrala <>
Soumis le : jeudi 22 janvier 2015 - 14:38:10
Dernière modification le : jeudi 24 septembre 2020 - 16:36:02
Archivage à long terme le : : jeudi 23 avril 2015 - 10:30:58

Fichier

A-593.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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⟩

Partager

Métriques

Consultations de la notice

454

Téléchargements de fichiers

84