A Taste of Sound Reasoning in Faust

Abstract : We address the question of what software verification can do for the audio community by showcasing some preliminary design ideas and tools for a new framework dedicated to the formal reasoning about Faust programs. We use as a foundation one of the strongest current proof assistants, namely Coq combined with SSReflect. We illustrate the practical impact of our approach via a use case, namely the proof that the implementation of a simple low-pass filter written in the Faust audio programming language indeed meets one of its specification properties. The paper thus serves three purposes: (1) to provide a gentle introduction to the use of formal tools to the audio community, (2) to put forward programming and formal reasoning paradigms we think are well suited to the audio domain and (3) to illustrate this approach on a simple yet practical audio signal processing example, a low-pass filter.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal-mines-paristech.archives-ouvertes.fr/hal-01251069
Contributeur : Claire Medrala <>
Soumis le : mardi 5 janvier 2016 - 15:45:33
Dernière modification le : lundi 12 novembre 2018 - 10:57:01
Document(s) archivé(s) le : jeudi 7 avril 2016 - 15:28:49

Fichier

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

Identifiants

  • HAL Id : hal-01251069, version 1

Citation

Emilio Jesús Gallego Arias, Olivier Hermant, Pierre Jouvelot. A Taste of Sound Reasoning in Faust. The Linux Audio Conference (LAC 2015) , Johannes Gutenberg University (JGU), Apr 2015, Mainz, Germany. ⟨hal-01251069⟩

Partager

Métriques

Consultations de la notice

227

Téléchargements de fichiers

120