Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

### lunes 14 de marzo de 2011

11:00am IMDEA conference room

**Thomas Dillig***, PhD Student**, Stanford University, USA*

### Program Paths Simplified: Scalable Path-Sensitive Analysis without Heuristics

#### Abstract:

A path-sensitive static analysis considers each possible
execution path through a program separately, potentially yielding much
more precise results than an analysis that makes fewer distinctions
among paths. While precise path-sensitive reasoning is known to be
necessary to prove many interesting facts about programs, fully
path-sensitive analyses have not scaled well because standard
representations of program paths quickly grow out of control.

In this talk, I will describe two techniques that allow path-sensitive
program analyses to scale. I will first introduce on-line constraint
simplification, which eliminates redundant subparts of logical
formulas used to distinguish execution paths. In practice, the
formulas used to describe program paths are highly redundant; thus,
techniques for keeping path formulas concise can have a dramatic
impact on analysis scalability. A second, complementary technique
reduces formula size even further: Because static analyses are
typically only interested in answering may (i.e., satisfiability) and
must (i.e., validity) queries, I will show how to extract from the
original path formulas a pair of satisfiabilty- and
validity-preserving formulas that contain many fewer variables and
that are as good as the original path formula for answering may and
must queries about the program. I will demonstrate that these
techniques allow a fully path-sensitive analysis to scale to very
large, multi-million line programs for the first time.