Campus Event Calendar
Event Entry
What and Who
Compositional Shape Analysis by means of Bi-Abduction
Cristiano Calcagno
Imperial College, London
SWS Colloquium
SWS, RG1
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 8 March 2010
11:00
90 Minutes
E1 5
5th floor
Saarbrücken
Abstract
We describe a compositional shape analysis, where each
procedure is analyzed independently of its callers. The analysis
uses an abstract domain based on a restricted fragment of separation
logic, and assigns a collection of Hoare triples to each procedure;
the triples provide an over-approximation of data structure
usage. Compositionality brings its usual benefits - increased potential
to scale, ability to deal with unknown calling contexts, graceful
way to deal with imprecision - to shape analysis, for the first time.
The analysis rests on a generalized form of abduction (inference
of explanatory hypotheses) which we call bi-abduction. Bi-abduction
displays abduction as a kind of inverse to the frame problem:
it jointly infers anti-frames (missing portions of state) and
frames (portions of state not touched by an operation), and is the
basis of a new interprocedural analysis algorithm. We have implemented
our analysis algorithm and we report case studies on
smaller programs to evaluate the quality of discovered specifications,
and larger programs (e.g., an entire Linux distribution) to test
scalability and graceful imprecision.
procedure is analyzed independently of its callers. The analysis
uses an abstract domain based on a restricted fragment of separation
logic, and assigns a collection of Hoare triples to each procedure;
the triples provide an over-approximation of data structure
usage. Compositionality brings its usual benefits - increased potential
to scale, ability to deal with unknown calling contexts, graceful
way to deal with imprecision - to shape analysis, for the first time.
The analysis rests on a generalized form of abduction (inference
of explanatory hypotheses) which we call bi-abduction. Bi-abduction
displays abduction as a kind of inverse to the frame problem:
it jointly infers anti-frames (missing portions of state) and
frames (portions of state not touched by an operation), and is the
basis of a new interprocedural analysis algorithm. We have implemented
our analysis algorithm and we report case studies on
smaller programs to evaluate the quality of discovered specifications,
and larger programs (e.g., an entire Linux distribution) to test
scalability and graceful imprecision.
Contact
Claudia Richter
9325 688
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
206
passcode not visible
logged in users only
Claudia Richter, 03/11/2010 16:22
Claudia Richter, 03/04/2010 10:44 -- Created document.
Claudia Richter, 03/04/2010 10:44 -- Created document.