SEMINAR
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