Time+Place: Tuesday 02/12/2014 14:30 Room 337-8 Taub Bld.
Title: Principles of Shape Analysis
Speaker: Mooly Sagiv - Colloquium Lecture http://www.math.tau.ac.il/~msagiv/
Affiliation: Tel-Aviv University
Host: Erez Petrank

Abstract:

In program analysis, a shape analysis is a static code analysis technique
that discovers and verifies properties of linked, dynamically allocated data
structures in (usually imperative) computer programs. For example,
discriminating between cyclic and acyclic lists and proving that two data
structures cannot access the same piece of memory. More generally, shape
analysis discovers quantified invariants of strongly dynamic software
systems.

In the first part of this talk, I will describe applications of shape
analysis including traditional ones like memory safety and preservation of
data structure invariants, as well as new applications including
verification of web servers and software defined networks.
I will then show that how to harness automatic deduction methods to perform
shape analysis.
Finally, I will sketch alternatives to shape analysis for programs with
composite data structures.

The first part of this talk is based on a joint work with Thomas Reps and
Reinhard Wilhelm. The second part of is also based on a joint work with
Kalev Alpernas, Thomas Ball, Nikolaj Bjorner,  Ken McMillan, and Thomas
Reps.
The third part of the talk is based on a joint work with Alex Aiken,
Kathleen Fisher, Guy Golan-Gueta, Peter Hawkins, G. Ramalingam, Martin
Rinard, Ohad Shcham,  Martin Vechev, Eran Yahav, and Ofri Ziv

Short Bio: 
Mooly Sagiv is Professor of Computer Science at Tel Aviv University.
His research focuses on program analysis and verification, in particular
reasoning about imperative programs manipulating dynamic data structures.
His current work includes shape analysis and reasoning about software
defined networks. Sagiv is a recipient of a 2013 senior ERC research grant 
for Verifying and Synthesizing Software Composition.

Sagiv was a visiting professor at UC Berkeley and Stanford University in
2010-2011, and was a Postdoc with Tom Reps at The University of Wisconsin in
1994-1995.  He spent 3 years at IBM as a researcher after earning his PhD
from the Technion Israel in 1991.


Desserts will be served from 14:15
Lecture starts at 14:30