Waterloo Programming Languages Seminars

Previous terms: W11 F10 S10 F08 S08 W08 F07 W07 F06 S06 W06

Current term:

Date Speaker Title (click for abstract) Location
Mon. July 4, 2011 at 1:30 pm Pavel Parízek Randomized Backtracking in State Space Traversal DC 1304
Fri. July 22, 2011 at 10:00 am Michael Pradel Large-Scale API Protocol Mining for Automated Bug Detection E5 4106

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:

The purpose is for us all to see what people are interested in, and motivate discussions.


Randomized Backtracking in State Space Traversal

Pavel Parízek
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

Michael Pradel
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.