Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Domain Specific Languages for Verified Software
Speaker:Damien Zufferey
coming from:MIT
Speakers Bio:Damien Zufferey is a Postdoctoral researcher in Martin Rinard's group at MIT
CSAIL since Octorber 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.
Event Type:SWS Colloquium
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Date, Time and Location
Date:Monday, 15 August 2016
Duration:90 Minutes
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 an 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.

Name(s):Susanne Girard
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):

Susanne Girard/MPI-SWS, 08/10/2016 03:07 PM
Last modified:
halma/MPII/DE, 12/01/2016 12:00 AM
  • Susanne Girard, 08/10/2016 03:12 PM -- Created document.