Campus Event Calendar
Event Entry
What and Who
Domain Specific Languages for Verified Software
Damien Zufferey
MIT
SWS Colloquium
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.
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 15 August 2016
10:30
90 Minutes
G26
111
Kaiserslautern
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 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.
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.
Contact
Susanne Girard
--email hidden
passcode not visible
logged in users only
Susanne Girard, 08/10/2016 15:12 -- Created document.