Wed 28 Oct 2015 11:37 - 12:00 at Grand Station 1 - 1. Model Checking Chair(s): Julian Dolby

Modern event-driven applications, such as, web pages and mobile apps, rely on asynchrony to ensure smooth end-user experience. Unfortunately, even though these applications are executed by a single event-loop thread, they can still exhibit nondeterministic behaviors depending on the execution order of interfering asynchronous events. As in classic shared-memory concurrency, this nondeterminism makes it challenging to discover errors that manifest only in specific schedules of events. In this work we propose the first stateless model checker for event-driven applications, called R4. Our algorithm systematically explores the nondeterminism in the application and concisely exposes its overall effect, which is useful for bug discovery. The algorithm builds on a combination of three key insights: (i) a dynamic partial order reduction (DPOR) technique for reducing the search space, tailored to the domain of event-driven applications, (ii) conflict-reversal bounding based on a hypothesis that most errors occur with a small number of event reorderings, and (iii) approximate replay of event sequences, which is critical for separating harmless from harmful nondeterminism. We instantiate R4 for the domain of client-side web applications and use it to analyze event interference in a number of real-world programs. The experimental results indicate that the precision and overall exploration capabilities of our system significantly exceed that of existing techniques.

Wed 28 Oct

Displayed time zone: Eastern Time (US & Canada) change

10:30 - 12:00
1. Model CheckingOOPSLA at Grand Station 1
Chair(s): Julian Dolby IBM Research
10:30
22m
Talk
Detecting Redundant CSS Rules in HTML5 Applications: A Tree Rewriting ApproachOOPSLA Artifact
OOPSLA
Anthony Widjaja Lin Yale-NUS College, Singapore, Matthew Hague Royal Holloway University of London, UK, C.-H. Luke Ong University of Oxford, UK
Link to publication
10:52
22m
Talk
SATCheck: SAT-Directed Stateless Model Checking for SC and TSOOOPSLA Artifact
OOPSLA
Brian Demsky University of California at Irvine, USA, Patrick Lam University of Waterloo, Canada
Link to publication
11:15
22m
Talk
Programming with Enumerable Sets of Structures
OOPSLA
Ivan Kuraj Massachusetts Institute of Technology, USA, Viktor Kunčak EPFL, Switzerland, Daniel Jackson Massachusetts Institute of Technology, USA
DOI
11:37
22m
Talk
Stateless Model Checking of Event-Driven Applications
OOPSLA
Casper Svenning Jensen Aarhus University, Denmark, Anders Møller Aarhus University, Veselin Raychev ETH Zurich, Switzerland, Dimitar Dimitrov ETH Zurich, Switzerland, Martin Vechev ETH Zurich, Switzerland
DOI