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

[Aaron Turon]

Carl will postpone his talk till Aug 4.  We currently have no talks
scheduled for July, in part because of conference deadlines.  If you
are not preparing a paper and would like to give a talk, please let me
know!

Cheers,
Aaron

On Fri, Jun 27, 2008 at 1:35 AM, Daniel Brown <dbrown at ccs.neu.edu> wrote:
> This conflicts with Carl's research talk. I'm interested in this; are
> others?
>
> On Thu, Jun 26, 2008 at 12:51 PM, Mitchell Wand <wand at ccs.neu.edu> wrote:
>>>
>>> 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
>>>
>>> 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
>>
>>
>>
>>
>>
>> _______________________________________________
>> pl-seminar mailing list
>> pl-seminar at lists.ccs.neu.edu
>> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar
>>
>
>
> _______________________________________________
> Pl-sem-jr mailing list
> Pl-sem-jr at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-sem-jr
>
>