[Colloq] Hiring Talk, Tuesday, March 17 - Domagoj Babic

[Rachel Kalweit]

The College of Computer and Information Science presents a Hiring Talk by:
Domagoj Babic - University of British Columbia 

Tuesday, March 17 at 1:30pm
366 West Village H.

Title:
 ------
Scalable and Precise Extended Static Checking

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.

Host: Pete Manolios