University of Illinois at Urbana-Champaign Block I logo
university of illinois at urbana-champaign

Department of Computer Science

Back to Listing

I2PC Seminar Series - Milos Gligoric (University of Illinois)

Event Type
Illinois-Intel Parallelism Center
Siebel Center 2405
Apr 18, 2013   4:00 - 5:00 pm   Central Time
Milos Gligoric (University of Illinois)
Originating Calendar
I2PC Events

Illinois-Intel Parallelism Center (I2PC) Distinguished Speaker Series

Thursday, April 18th, 4-5pm Central Time, Siebel Center 2405


                  Model Checking Database Applications

                                    Milos Gligoric
                                University of Illinois

ABSTRACT: We describe the design of DPF, an explicit-state model checker
for database-backed web applications. DPF interposes between the program
and the database layer, and precisely tracks the effects of queries made
to the database.  We experimentally explore several implementation
choices for the model checker: stateful vs. stateless search, state
storage and backtracking strategies, and dynamic partial-order
reduction. In particular, we define independence relations at different
granularity levels of the database (at the database, relation, record,
attribute, or cell level), and show the effectiveness of dynamic
partial-order reduction based on these relations.  We apply DPF to look
for atomicity violations in web applications. Web applications maintain
shared state in databases, and typically there are relatively few
database accesses for each request. This implies concurrent interactions
are limited to relatively few and well-defined points, enabling our
model checker to scale.  We explore the performance implications of
various design choices and demonstrate the effectiveness of DPF on a set
of Java benchmarks.  Our model checker was able to find new concurrency
bugs in two open-source web applications, including in a standard
example distributed with the Spring framework.

BIO: Milos Gligoric is a PhD student in the Department of Computer
Science at the University of Illinois at Urbana-Champaign.  He works
with Prof. Darko Marinov on Software Testing and Software Model
Checking.  Milos' work has been supported by the C.L. & Jane W-S. Liu
Award, Max Planck Institute internship, Saburo Muroga fellowship,
NASA/MCT internship, IBM X10 innovation award, and Intel internship.


The talk will be streamed live at this link:

Questions to the speaker for live response can be directed to our chat

A complete list of seminars (with archived copies of past talks) is
available here:

link for robots only