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:Programming Abstractions for Verifiable Software
Speaker:Damien Zufferey
coming from:Max Planck Institute for Software Systems
Speakers Bio:
Event Type:Joint Lecture Series
Visibility:D1, D2, D3, INET, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Wednesday, 15 May 2019
Duration:60 Minutes
Building:E1 5
In this talk, I will show how we can harness the synergy between programming

languages and verification methods to help programmers build reliable software.
First, we will look at fault-tolerant distributed algorithms. These algorithms
are central to any high-availability application but they are notoriously
difficult to implement due to asynchronous communication and faults. A fault-
tolerant consensus algorithms which can be described in ~50 lines of pseudo
code can easily turns into a few thousand lines of actual code. To remediate
this, I will introduce PSync a domain specific language for fault-tolerant
distributed algorithms. The key insight is the use of communication-closure
(logical boundaries in a program that messages should not cross) to structure
the code. Communication-closure gives a syntactic scope to the communication,
provides some form of logical time, and give the illusion of synchrony. These
element greatly simplify the programming and verification of fault-tolerant
In the second part of the talk, we will discuss a new project exploring how
advances in rapid prototyping (3D printers) may impact how we develop software
for robots. These advances may soon be enable adding computational elements as
part of the internal structure of objects. The goal of this project is to
rethink the software/hardware boundary and integrate the two together. I will
present a system we are developing where components integrate for geometry
(hardware) and behavior (software). The system allows from bottom-up composition
and top-down decomposition. The bottom-up composition connects components
together to achieve more complex behaviors. The top-down decomposition project a
global specification on the individual components and performs verification at
the level of individual components.

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

Jennifer Müller/MPI-INF, 02/27/2019 02:25 PM
Last modified:
Uwe Brahm/MPII/DE, 05/15/2019 07:01 AM
  • Jennifer Müller, 02/27/2019 02:26 PM -- Created document.