Wed Dec 2, 2009, 11:00-12:00, 4760 Boelter Hall

Deskcheck: A System for Creating Specialized Shape Analyzers
of Composite Shared Representations

Mooly Sagiv
Tel Aviv University (visiting Stanford)

We describe a new system, Deskcheck, which supports the creation of static
analyzers that are able to establish properties of programs that
manipulate dynamically allocated memory, arrays, and integers.
The novel feature of Deskcheck is its ability to establish quantified
invariants over mixed domains, e.g., heap and numeric domains, while
using separate implementations of the different domains, plus a
mechanism for them to communicate, involving a few simple primitives.

We describe the use of Deskcheck to develop an abstract interpreter
that combines heap and numeric domains, as well as its use to
analyze an existing web server that makes use of complex shared
arrays and dynamically allocated memory, as well as explicit
(programmer-managed) reference counting.

If time permits, I will also describe other ongoing projects with colleges
at UCB, Stanford, and TAU.

Joint work with Bill McCloskey, UCB and Thomas Reps, U. Wisconsin, Madison.


About the speaker:  Mooly Sagiv received his PhD from the Technion Israel
in 1990. He then joined IBM Haifa Research group as a research staff member.
In 1994-95, he was working as a visiting researcher with Bob Paige and
Tom Reps in DIKU, and Wisconsin. In 1996 he was a visiting professor at
the University of Chicago until he joined Tel Aviv university as a
faculty member. He was on sabbatical last year at UCB visiting Ras Bodik
and is on sabbatical this year at Stanford University visiting Alex Aiken.
Mooly is married to Tamar and has three little daughters Aya, Naama, and
Hagar.  In his spare time, he likes to run and completed few marathons
including: Tromsoe, Chicago, Toronto, Duluth, Boston, Tiberias, Big Sur,
and New York.

Host: Jens Palsberg