FACULTY CANDIDATE: Swarat Chaudhuri - FACULTY CANDIDATE University of Pennsylvania Context-Sensitive Software Model Checking ACES 2.302. Tuesday March 20 2007 at 11:00 a.m.

Contact Name: 
Jenna Whitney
Mar 20, 2007 11:00am - 12:00pm

There is a signup schedule for this event.<

Speaker Name/Affiliation: Swarat Chaudhuri

University of Pennsylvania

Date/Time: Tuesday March 20 2007
11:00 a.m. - Noon

Coffee: 10:45 a.m.

Location: ACES 2.302<

Host: Jayadev Misra

Talk Title: Context-Sensitive Software

Model Checking

Talk Abstract:
Software model checking an algorit

specification-driven approach to software
analysis has emerg

ed as an active area
of research in the last few years producing
number of successful tools. While work in
this area builds on the 25-y

ear-old literature
on model checking of finite-state systems it

s to grapple with several additional issues.
A crucial one is that cont

rol flow of procedural
programs depends on contexts defined by the

call stack so that any reasonably precise
software model checker needs
to analyze pushdown
models of programs rather than finite-state ones.<

In this talk I address two main components
of such context-sens

itive model checking:
requirement specification and algorithmic

lysis. The first---and main---story starts
with the observation that te

mporal specification
logics like the mu-calculus while mainstays of traditional model checking cannot specify
context-sensitive program

requirements such as:
A file is read before control leaves the current

procedural context. The difficulty is that the
mu-calculus is only

as expressive as tree automata
and thus cannot reason about the nestin

g of
contexts. A way to overcome this issue I
demonstrate is to v

iew a program as a generator
not of a computation tree but of a graph

a nested tree. Temporal logics interpreted
on this ne

w structure are now defined and the
model checking problem is re-phras

ed as: Does
the nested tree generated by a program satisfy
a proper

ty? Not only does this tweak let us
state many new requirements but it
does so
without changing the complexity of model-checking.
There a

re other positives: for example a fixpoint
calculus on nested trees th

at we define allows
symbolic model-checking and modular specifications

and has an automata-theoretic characterization
similar to that for
the mu-calculus.

Next I address the reachability problem for

shdown automata an algorithmic problem central
to software model check

ing that also shows up in
contexts such as slicing alias analysis sha

analysis and type-based flow analysis. In a
recent result I ha

ve used a form of preprocessing
to improve (slightly but asymptoticall

y) the thirty-
something years old cubic solution to this problem

lso answering the question of whether its many
applications suffer from
an intrinsic cubic bottleneck.
I briefly sketch the technique as well
as suggest
how the core idea of the algorithm may find general
in heuristic design for software analysis.