VERIMAG
2 avril 2009 - 14h00
Scalable and Precise Extended Static Checking
par Domagoj Babic de Fujitsu Labs America
Abstract: Automatic software verification and bug finding have been a long-held
goal in software engineering. Many techniques exist, trading off
varying levels of automation, coverage, precision, and scalability.
Extended Stating Checking (ESC), a combination of static checking and
decision procedures has emerged as a powerful technique for improving
software reliability. A major limitation of the ESC paradigm is that
it requires programmers to write tedious pre- and post-conditions for
every function, something that programmers have not widely embraced.
One way around this restriction is to perform a whole-program
interprocedural analysis. Unfortunately, previously known scalable
interprocedural analyses are not precise enough for verification
purposes. This talk presents a practical new technique for scalable
interprocedural path-sensitive analysis, named structural abstraction,
prototyped in the Calysto extended static checker. While structural
abstraction eliminates the need for manual code annotation with pre- and
post-conditions, it imposes a heavy burden on decision procedures
because it requires checking the validity of large, complex logical
formulas (i.e., verification conditions). The second topic of this talk
is a novel approach to solving such large verification conditions. The
presented approach gave a 100-fold improvement in performance over the
best previously known approaches, significantly improving the usability
of modern ESC tools. Thanks to these advancements, Calysto discovered
dozens of bugs, completely automatically, in hundreds of thousands of
lines of production, open-source applications, with a very low rate of
false error reports.
Bio:
- ---
Domagoj Babic received his Dipl.Ing. in Electrical Engineering and
M.Sc. in Computer Science from the Zagreb University (Faculty of
Electrical Engineering and Computing) in 2001 and 2003. He received
his Ph.D. in Computer Science in 2008 from the University of
British Columbia. Domagoj was a recipient of Microsoft Research
Graduate Fellowship in 2005.
Domagoj's research currently focuses on automatic software bug-finding
and verification techniques for large programs. More broadly, Domagoj
is interested in concurrent programs, software testing, security
analysis of web applications, decision procedures, and the application
of formal software analysis to other areas, like low-power software
optimization.
Domagoj Babic est candidat à Verimag sur le poste de CR2 CNRS
