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

[Daniel Brown]

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 <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
>>
>
>
>
>
>
> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar
>
>
-------------- next part --------------
HTML attachment scrubbed and removed