Tight Localization of Abstract Memories for Scalable Semantics-based Static Analysis

Speaker:	Professor Kwangkeun YI
		School of Computer Science and Engineering
		Seoul National University

Title:		"Tight Localization of Abstract Memories for Scalable
		 Semantics-based Static Analysis"

Date:		Monday, 15 November 2010

Time:		4:00pm - 5:00pm

Venue:		Lecture Theater F (near lifts 25/26), HKUST

Abstract:

I will present our works on developing an industrial-strength static
analyzers for finding memory-safety bugs in C programs. In particular, I
would like to present our recent technology that can substantially reduce
the memory footprint of our dense semantic analysis. The technology is an
improvement of existing "abstract garbage collection" in static analysis
or "framing" technology in software verification. Our technique first
estimates, by an efficient pre-analysis, the set of abstract locations
that will be accessed (not reachable) during the analysis of each program
block. Then the main analysis uses the access-set results to trim the
memory entries before analyzing the program blocks. In experiments with a
realistic global C static analyzers, the technique can reduce the memory
consumption by 70-90%, without sacrificing the anlaysis precision.

(This is co work with Hakjoo Oh and Lucas Brutschy)


********************
Biography:

Kwangkeun Yi (PhD 1993, UIUC) is a professor of Seoul National University
and a director of the ROSAEC (Research on Software Analysis for Error-free
Computing) Center (http://rosaec.snu.ac.kr), a national  center of
excellence in static analysis, software verification and programming
languages. His work has been on static program analysis, higher-order &
typed programming language theory, and systems application of static
analysis. His homepage is http://ropas.snu.ac.kr/~kwang