Waterloo Programming Languages Seminars
All are welcome.
Talk announcements are also posted to a public mailing list.
To volunteer to give a talk, contact Ondřej Lhoták.
Talks can range from informal to formal, and they can be
about any of the following:
- completed research
- research that you plan to start ("half-baked ideas" to be critiqued by your peers)
- interesting paper(s) you have read
The purpose is for us all to see what people are interested in,
and motivate discussions.
Randomized Backtracking in State Space Traversal
July 4, 2011
While exhaustive state space traversal is not feasible in reasonable
time for complex concurrent programs, many techniques for efficient
detection of concurrency errors and testing of concurrent programs
have been introduced in recent years, such as directed search and
context-bounded model checking. We propose to use depth-first traversal
with randomized backtracking, where it is possible to backtrack from
a state before all outgoing transitions have been explored, and the
whole process is driven by random number choices. Experiments with a
prototype implementation in JPF on several Java programs show that, in
most cases, fewer states must be explored to find an error with our
approach than using the existing techniques.
Large-Scale API Protocol Mining for Automated Bug Detection
July 22, 2011
Programmers using an API often must respect protocols that specify the
order in which methods should be called. Violations of such protocols
lead to unexpected behavior, incorrect results, and even program
crashes. Unfortunately, few APIs provide formal specifications of method
ordering constraints, making it hard for programmers to understand the
protocols and difficult for program analyses to find protocol violations.
This talk presents an automated approach to infer API protocols from
existing programs based on the assumption that these programs use the
API correctly in most cases. We present a scalable, dynamic analysis
that infers formal specifications of method call ordering constraints.
The mined protocols enable automated bug detection by feeding them into
runtime verifiers and static checkers of API clients. To evaluate the
approach, we perform extensive studies with real-world Java programs and
popular APIs. The results show that our approach infer useful protocols
that help finding serious bugs.
Michael Pradel is a PhD student at ETH Zurich. His primary research
interests are in the area of software engineering and programming
languages. In particular, he is interested in automated program analyses
for finding programming errors. Michael graduated in computer science at
Technical University in Dresden, Germany. He also spent two years at
Ecole Centrale Paris, France, where he became a graduate engineer, and
visited EPFL, Switzerland, to pursue his master thesis.