Dr. Damien Zufferey
Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology
Invited by PROFESSOR Krzysztof Czarnecki
ALL ARE WELCOME!
Abstract:
In
this
talk,
I
will
show
how
we
can
harness
the
synergy
between
programming
languages
and
verification
methods
to
help
programmers
build
reliable
software,
prove
complex
properties
about
them,
and
scale
verification
to
industrial
projects.
First, I will describe P a domain-specific language to write asynchronous event driven code. P isolates the control-structure, or protocol, from the data-processing. This allows us not only to generate efficient code, but also to test it using model checking techniques. P was used to implement and verify the core of the USB device driver stack that ships with Microsoft Windows 8 and later versions. The language abstractions and verification helped building a driver which is both reliable and fast.
Then, I will introduce PSync a domain specific language for fault-tolerant distributed algorithms that simplifies the implementation of these algorithms, enables automated formal verification, and can be executed efficiently. Fault-tolerant algorithms are notoriously difficult to implement correctly, due to asynchronous communication and faults. PSync provides a high-level abstraction by viewing an asynchronous faulty system as synchronous one with an adversarial environment that simulates faults. We have implemented in PSync several important fault-tolerant distributed algorithms and we compare the implementation of consensus algorithms in PSync against implementations in other languages.
Biography:
Damien
Zufferey
is
a
Postdoctoral
researcher
in
Martin
Rinard's
group
at
MIT
CSAIL
since
October
2013.
Before
moving
to
MIT,
He
obtained
a
PhD
at
the
Institute
of
Science
and
Technology
Austria
(IST
Austria)
under
supervision
of
Thomas
A.
Henzinger
in
September
2013
and
a
Master
in
computer
science
from
EPFL
in
2009.
He
is
interested
in
improving
software
reliability
by
developing
theoretical
models,
building
analysis
tools,
and
giving
the
programmer
the
appropriate
language
constructs.
He
is
particularly
interested
in
the
study
of
complex
concurrent
systems.
His
research
lies
at
the
intersection
of
formal
methods
and
programming
languages