Campus Event Calendar
Event Entry
What and Who
Algorithms and Tools for Verification and Testing of Asynchronous Programs
Zilong Wang
MMCI
SWS Student Defense Talks - Thesis Defense
SWS
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 10 March 2016
15:30
60 Minutes
G26
111
Kaiserslautern
Abstract
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.
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.
Contact
--email hidden
Video Broadcast
Yes
Saarbrücken
E1 5
029
passcode not visible
logged in users only
Maria-Louise Albrecht, 02/03/2016 11:14
Maria-Louise Albrecht, 02/02/2016 09:58 -- Created document.
Maria-Louise Albrecht, 02/02/2016 09:58 -- Created document.