2:30 pm, 1257 CS (Cookies: 3:30 pm, 2310 CS)
Programming Languages Seminar: G. Ramalingam, IBM Hawthorne Research Center,
"Verifying Safety Properties using Separation and Heterogeneous Abstraction"
The increasingly important and critical role that software is playing has
led to an increasing recognition of the need for more reliable, secure, and
safe software. This has led to a significant focus on static verification of
software properties in the recent years -- ensuring that a program satisfies
certain safety properties, without running it. While significant advances
have been made in this respect, developing verification techniques that are
simultaneously precise and scalable enough continues to be a challenge.
In this talk, we show how separation (decomposing a verification problem
into a collection of verification subproblems) can be used to improve the
efficiency and precision of verification of safety properties. We present a
simple language for specifying separation strategies for decomposing a sin-
gle verification problem into a set of subproblems. (The strategy specifica-
tion is distinct from the safety property specification and is specified
separately.) We present a general framework of heterogeneous abstraction
that allows different parts of the heap to be abstracted using different
degrees of precision at different points during the analysis. We show how
the goals of separation (i.e., more efficient verification) can be realized
by first using a separation strategy to transform (instrument) a verifica-
tion problem instance (consisting of a safety property specification and an
input program), and by then utilizing heterogeneous abstraction during the
verification of the transformed verification problem.
(Joint work with Eran Yahav.)
![[Computer Systems Lab]](http://www.cs.wisc.edu/pics/csl_logo.gif){kind=logo}