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 su
ch that a) they are written in a convenient\, high-level language\, b) ope
rational semantics are real-time and reasonably efficient\, and c) the ove
rhead of mechanized verification remains low.
Tailored to this purpose\,
we introduce a domain-specific functional programming language: W; W is a
n extended call-by-value λ-calculus with feedback and synchronous semanti
cs\, designed to be flexible enough so DSP algorithms can be written in it
--- still distinguishing different implementation forms --- but permittin
g an easy embedding into the Coq proof assistant for mechanization.
We w
ill present the syntax and denotational semantics of W\, and their Coq imp
lementation. Our first use case will be to prove in Coq that every W progr
am of a restricted syntactic subset is linear-time invariant. To do that\,
we characterize the LTI property using a logical relation\, which require
s to extend LTI to open programs as usual.
The denotational semantics ar
e convenient for mechanized reasoning\, however still incur in re-computat
ion of previous steps. We will introduce a more operational version of the
semantics using a notion of imperative update\, providing an execution mo
del much closer to actual low-level implementation.
The semantics are pr
esented 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 prov
e 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 as
pects of Digital Signal Processing algorithms. In particular\, we are inte
rested in the high-level theory of Linear-Time-Invariant (LTI) systems\, i
ncluding typical algorithms such as filters and resonators in their differ
ent implementations.
Our goal is to develop a setting for reasoning abou
t DSP algorithms such that a) they are written in a convenient\, high-leve
l language\, b) operational semantics are real-time and reasonably efficie
nt\, and c) the overhead of mechanized verification remains low.
Tailore
d 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 c
an be written in it --- still distinguishing different implementation form
s --- but permitting an easy embedding into the Coq proof assistant for me
chanization.
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 inva
riant. To do that\, we characterize the LTI property using a logical relat
ion\, which requires to extend LTI to open programs as usual.
The denota
tional semantics are convenient for mechanized reasoning\, however still i
ncur in re-computation of previous steps. We will introduce a more operati
onal version of the semantics using a notion of imperative update\, provid
ing an execution model much closer to actual low-level implementation.
T
he semantics are presented as an interpreter\, which we study in two ways:
first\, we produce an executable version of some example programs by stag
ing 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 tradi
tional synchronous domain do\, requiring the use of global invariants; we
will discuss if the situation can be improved.
DTSTAMP:20190522T174434Z
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