LAC 2015: Video: "A Taste of Sound Reasoning" by Emilio Jesús Gallego Arias, Oliver Hermant, Pierre Jouvelot
Linux Audio Conference 2015
A Taste of Sound Reasoning
Emilio Jesús Gallego Arias, Oliver Hermant, Pierre Jouvelot
 288p  576p 

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 import 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.

The video is licensed in terms of the Creative Commons Attribution-ShareAlike 3.0 Unported License. Attribute to All copyright(s) remain with the author/speaker/presenter.