Campus Event Calendar
Event Entry
What and Who
On Inter-Procedural Analysis of Programs with Lists and Data
Cezara Dragoi
LIAFA Université Paris Diderot
SWS Colloquium
SWS, RG1
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 28 April 2011
14:15
75 Minutes
Uni Kaiserlautern, building 48
680
Kaiserslautern
Abstract
We address the problem of automatic synthesis of assertions on
sequential programs with singly-linked lists containing data over
infinite domains such as integers or reals. Our approach is based on an
accurate abstract inter-procedural analysis.
We define compositional techniques for computing procedure summaries
concerning various aspects such as shapes, sizes, and data.
Relations between program configurations
are represented by graphs where vertices represent list segments
without sharing.
The data in the these list segments are characterized by constraints
in new complex abstract domains.
We define an abstract domain whose elements correspond to an expressive class
of first order universally quantified formulas and an abstract domain of multisets.
Our analysis computes the effect of each procedure in a local
manner, by considering only the reachable parts of the heap from its
actual parameters.
In order to avoid losses of information, we introduce
a mechanism based on unfolding/folding operations allowing
to strengthen the analysis in the domain of first-order formulas by
the analysis in the multisets domains.
The same mechanism is used for strengthening the sound (but
incomplete) entailment operator of the domain of first-order formulas.
We have implemented our techniques in a prototype tool and
we have shown that our approach is powerful enough for automatic
(1) generation of non-trivial procedure summaries, (2) pre/post-
condition reasoning.
sequential programs with singly-linked lists containing data over
infinite domains such as integers or reals. Our approach is based on an
accurate abstract inter-procedural analysis.
We define compositional techniques for computing procedure summaries
concerning various aspects such as shapes, sizes, and data.
Relations between program configurations
are represented by graphs where vertices represent list segments
without sharing.
The data in the these list segments are characterized by constraints
in new complex abstract domains.
We define an abstract domain whose elements correspond to an expressive class
of first order universally quantified formulas and an abstract domain of multisets.
Our analysis computes the effect of each procedure in a local
manner, by considering only the reachable parts of the heap from its
actual parameters.
In order to avoid losses of information, we introduce
a mechanism based on unfolding/folding operations allowing
to strengthen the analysis in the domain of first-order formulas by
the analysis in the multisets domains.
The same mechanism is used for strengthening the sound (but
incomplete) entailment operator of the domain of first-order formulas.
We have implemented our techniques in a prototype tool and
we have shown that our approach is powerful enough for automatic
(1) generation of non-trivial procedure summaries, (2) pre/post-
condition reasoning.
Contact
Maria-Louise Maggio
9604
--email hidden
passcode not visible
logged in users only
Maria-Louise Maggio, 04/26/2011 11:18 -- Created document.