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:Algorithms and Tools for Verification and Testing of Asynchronous Programs
Speaker:Zilong Wang
coming from:Max Planck Institute for Software Systems
Speakers Bio:
Event Type:SWS Student Defense Talks - Thesis Defense
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Thursday, 10 March 2016
Duration:60 Minutes
Software is becoming increasingly concurrent: parallelization, decentralization, and reactivity necessitate asynchronous programming in which processes communicate by posting messages/tasks to others’ message/task buffers. Asynchronous programming has been widely used to build fast servers and routers, embedded systems and sensor networks, and is the basis of Web programming using Javascript. Languages such as Erlang and Scala have adopted asynchronous programming as a fundamental concept with which highly scalable and highly reliable distributed systems are built.

Asynchronous programs are challenging to implement correctly: the loose coupling between asynchronously executed tasks makes the control and data dependencies diffi- cult to follow. Even subtle design and programming mistakes on the programs have the capability to introduce erroneous or divergent behaviors. As asynchronous programs are typically written to provide a reliable, high-performance infrastructure, there is a critical need for analysis techniques to guarantee their correctness.

In this dissertation, I provide scalable verification and testing tools to make asyn- chronous programs more reliable. I show that the combination of counter abstraction and partial order reduction is an effective approach for the verification of asynchronous systems by presenting PROVKEEPER and KUAI, two scalable verifiers for two types of asynchronous systems. I also provide a theoretical result that proves a counter- abstraction based algorithm called expand-enlarge-check, is an asymptotically optimal algorithm for the coverability problem of branching vector addition systems as which many asynchronous programs can be modeled. In addition, I present BBS and LL- SPLAT, two testing tools for asynchronous programs that efficiently uncover many sub- tle memory violation bugs.
Video Broadcast
Video Broadcast:YesTo Location:Saarbrücken
To Building:E1 5To Room:029
Tags, Category, Keywords and additional notes
Attachments, File(s):
Created:Maria-Louise Albrecht/MPI-KLSB, 02/02/2016 09:54 AM Last modified:Uwe Brahm/MPII/DE, 11/24/2016 04:13 PM
  • Maria-Louise Albrecht, 02/03/2016 11:14 AM
  • Maria-Louise Albrecht, 02/02/2016 09:58 AM -- Created document.