Max-Planck-Institut für Informatik
max planck institut
informatik
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
Language:English
Date, Time and Location
Date:Wednesday, 15 May 2019
Time:12:15
Duration:60 Minutes
Location:Saarbrücken
Building:E1 5
Room:002
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.
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
algorithms.
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.

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

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