[Pl-seminar] Dino Distefano @ Harvard Mon 6/30

[Mitchell Wand]

>
> Date: June 26, 2008 10:16:13 AM EDT
> To: programming at eecs.harvard.edu, ynot at seas.harvard.edu
> Subject: [Ynot] Monday, June 30 - Dino Distefano Talk
>
> Dino Distefano, from the Logic and Semantics Group in the Department of
> Computer Science at the University of London will here on Monday to give a
> talk from 2 - 3pm in MD 221.
> http://www.dcs.qmul.ac.uk/~ddino <http://www.dcs.qmul.ac.uk/%7Eddino>
>
> Please find his Title and Abstract below.
>
>
>
>
> TITLE: Compositional Shape Analysis
>
> ABSTRACT:
> In this talk we describe a compositional inter-procedural shape analysis,
> where each procedure is analyzed independently of its callers. The analysis
> performs proof search in 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 interprocedural algorithm rests on a new form of abduction (inference
> of explanatory hypotheses), which is used in our analysis algorithm to
> discover preconditions by abductive inference of missing heap portions.  We
> define a proof procedure for abduction, and use it to define our analysis
> algorithm.  We also report on the effects of the application of
> compositionality to a variety of
> large programs (up to >1 million LOC) by running experiments with an
> implementation of our algorithm.
> _______________________________________________
> Ynot mailing list
> Ynot at deas.harvard.edu
> https://lists.deas.harvard.edu/mailman/listinfo/ynot
>
-------------- next part --------------
HTML attachment scrubbed and removed