BEGIN:VCALENDAR
CALSCALE:GREGORIAN
VERSION:2.0
X-WR-TIMEZONE:Europe/Paris
METHOD:PUBLISH
PRODID:-//LIP6//www.lip6.fr//FR
X-WR-CALNAME;VALUE=TEXT:Séminaire LIP6
X-LIC-LOCATION:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
DTSTART:19810329T020000
TZNAME:GMT+02:00
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
DTSTART:19961027T030000
TZNAME:GMT+01:00
TZOFFSETTO:+0100
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:Towards verified modelling of Digital Signal Processing algorithms
ORGANIZER;CN=Emmanuel Chailloux:MAILTO:Emmanuel.Chailloux@lip6.fr
ATTENDEE;CN=Emilio J. Gallego Arias (MINES ParisTech);CUTYPE=INDIVIDUAL;PA
RTSTAT=ACCEPTED
DESCRIPTION:We study the formal verification of some aspects of Digital Si
gnal Processing algorithms. In particular\, we are interested in the high-
level theory of Linear-Time-Invariant (LTI) systems\, including typical al
gorithms such as filters and resonators in their different implementations
.
Our goal is to develop a setting for reasoning about DSP algorithms suc
h that a) they are written in a convenient\, high-level language\, b) oper
ational semantics are real-time and reasonably efficient\, and c) the over
head of mechanized verification remains low.
Tailored to this purpose\, w
e 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 implem
entation. 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 t
o extend LTI to open programs as usual.
The denotational semantics are co
nvenient for mechanized reasoning\, however still incur in re-computation
of previous steps. We will introduce a more operational version of the sem
antics using a notion of imperative update\, providing an execution model
much closer to actual low-level implementation.
The semantics are present
ed as an interpreter\, which we study in two ways: first\, we produce an e
xecutable version of some example programs by staging our interpreter with
MetaOCaml and study performance numbers; second\, we attempt to prove a c
orrespondence of the denotational and operational semantics formally. Here
\, we face similar problems as proofs in the traditional synchronous domai
n do\, requiring the use of global invariants; we will discuss if the situ
ation 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\, includi
ng typical algorithms such as filters and resonators in their different im
plementations.
Our goal is to develop a setting for reasoning about DSP a
lgorithms such that a) they are written in a convenient\, high-level langu
age\, b) operational semantics are real-time and reasonably efficient\, an
d c) the overhead of mechanized verification remains low.
Tailored to thi
s purpose\, we introduce a domain-specific functional programming language
: W; W is an extended call-by-value λ-calculus with feedback and synchron
ous semantics\, designed to be flexible enough so DSP algorithms can be wr
itten in it --- still distinguishing different implementation forms --- bu
t permitting an easy embedding into the Coq proof assistant for mechanizat
ion.
We will present the syntax and denotational semantics of W\, and the
ir Coq implementation. Our first use case will be to prove in Coq that eve
ry W program of a restricted syntactic subset is linear-time invariant. To
do that\, we characterize the LTI property using a logical relation\, whi
ch requires to extend LTI to open programs as usual.
The denotational sem
antics are convenient for mechanized reasoning\, however still incur in re
-computation of previous steps. We will introduce a more operational versi
on of the semantics using a notion of imperative update\, providing an exe
cution model much closer to actual low-level implementation.
The semantic
s are presented as an interpreter\, which we study in two ways: first\, we
produce an executable version of some example programs by staging our int
erpreter with MetaOCaml and study performance numbers; second\, we attempt
to prove a correspondence of the denotational and operational semantics f
ormally. Here\, we face similar problems as proofs in the traditional sync
hronous domain do\, requiring the use of global invariants; we will discus
s if the situation can be improved.
DTSTAMP:20190325T025500Z
DTSTART;TZID=Europe/Paris:20190221T160000
DURATION:PT2H
URL;VALUE=URI:https://www.lip6.fr/liens/organise-fiche.php?ident=O997
UID:LIP6/SEM/O997
LOCATION:Couloir 15-16 salle 101\, 4 place Jussieu - 75005 Paris
GEO:48.846954;2.354357
END:VEVENT
END:VCALENDAR