21/02/2019

Intervenant(s) : Emilio J. Gallego Arias (MINES ParisTech)

We study the formal verification of some aspects of Digital Signal Processing algorithms. In particular, we are interested in the high-level theory of Linear-Time-Invariant (LTI) systems, including typical algorithms such as filters and resonators in their different implementations.

Our goal is to develop a setting for reasoning about DSP algorithms such that a) they are written in a convenient, high-level language, b) operational semantics are real-time and reasonably efficient, and c) the overhead of mechanized verification remains low.

Tailored to this purpose, we introduce a domain-specific functional programming language: W; W is an extended call-by-value λ-calculus with feedback and synchronous semantics, designed to be flexible enough so DSP algorithms can be written in it --- still distinguishing different implementation forms --- but permitting an easy embedding into the Coq proof assistant for mechanization.

We will present the syntax and denotational semantics of W, and their Coq implementation. Our first use case will be to prove in Coq that every W program of a restricted syntactic subset is linear-time invariant. To do that, we characterize the LTI property using a logical relation, which requires to extend LTI to open programs as usual.

The denotational semantics are convenient for mechanized reasoning, however still incur in re-computation of previous steps. We will introduce a more operational version of the semantics using a notion of imperative update, providing an execution model much closer to actual low-level implementation.

The semantics are presented as an interpreter, which we study in two ways: first, we produce an executable version of some example programs by staging our interpreter with MetaOCaml and study performance numbers; second, we attempt to prove a correspondence of the denotational and operational semantics formally. Here, we face similar problems as proofs in the traditional synchronous domain do, requiring the use of global invariants; we will discuss if the situation can be improved.:

We study the formal verification of some aspects of Digital Signal Processing algorithms. In particular, we are interested in the high-level theory of Linear-Time-Invariant (LTI) systems, including typical algorithms such as filters and resonators in their different implementations.

Our goal is to develop a setting for reasoning about DSP algorithms such that a) they are written in a convenient, high-level language, b) operational semantics are real-time and reasonably efficient, and c) the overhead of mechanized verification remains low.

Tailored to this purpose, we introduce a domain-specific functional programming language: W; W is an extended call-by-value λ-calculus with feedback and synchronous semantics, designed to be flexible enough so DSP algorithms can be written in it --- still distinguishing different implementation forms --- but permitting an easy embedding into the Coq proof assistant for mechanization.

We will present the syntax and denotational semantics of W, and their Coq implementation. Our first use case will be to prove in Coq that every W program of a restricted syntactic subset is linear-time invariant. To do that, we characterize the LTI property using a logical relation, which requires to extend LTI to open programs as usual.

The denotational semantics are convenient for mechanized reasoning, however still incur in re-computation of previous steps. We will introduce a more operational version of the semantics using a notion of imperative update, providing an execution model much closer to actual low-level implementation.

The semantics are presented as an interpreter, which we study in two ways: first, we produce an executable version of some example programs by staging our interpreter with MetaOCaml and study performance numbers; second, we attempt to prove a correspondence of the denotational and operational semantics formally. Here, we face similar problems as proofs in the traditional synchronous domain do, requiring the use of global invariants; we will discuss if the situation can be improved.

Emmanuel.Chailloux (at) nulllip6.fr