[PRL] Fwd: Talk at Northeastern?

[Mitchell Wand]

I've scheduled Torben Amtoft to talk in pl-seminar on Wed 5/30.  Which of
the two topics would you all prefer to hear?  (Answer only if you're going
to be in town on 5/30 :-)

--Mitch

---------- Forwarded message ----------
From: Mitchell Wand <wand at ccs.neu.edu>
Date: May 15, 2007 2:14 PM
Subject: Re: Talk at Northeastern?
To: Torben Amtoft <tamtoft at cis.ksu.edu>

Our regular pl-seminar slot on Wed May 30th is open, so let's pencil you in
then.  I'll ask around to see which of the two topics would be of the most
interest.

See you then!  (Have you been in our shiny new building?)

--Mitch

On 5/15/07, Torben Amtoft <tamtoft at cis.ksu.edu> wrote:
>
> Hi Mitch,
>
>   I will be in Boston from May 24 to June 2.
> Would it be possible to give a talk at Northeastern?
> I have two talks in minds, with abstracts given below; please let me
> know which one (if any!) you think will be of most interest.
>
>   best regards
>
> Torben Amtoft
>
> --- Verification Condition Generation for Conditional Information Flow ---
>
> Abstract:
> We formulate an intraprocedural information flow analysis algorithm
> for sequential, heap manipulating programs.  We prove correctness of
> the algorithm, and argue that it can be used to verify some naturally
> occurring examples in which information flow is conditional on some
> Hoare-like state predicates being satisfied.  Because the correctness
> of information flow analysis is typically formulated in terms of
> noninterference of pairs of computations, the algorithm takes as input
> a program together with two-state assertions as postcondition, and
> generates two-state preconditions together with verification
> conditions.  To process heap manipulations and while loops, the
> algorithm must additionally be supplied two-state "object flow
> invariants" as well as two-state "loop flow invariants" which are
> themselves possibly conditional.
>
> This is joint work with Anindya Banerjee.
> http://www.cis.ksu.edu/~tamtoft/Papers/Amt+Ban:CondInfFlow-2007/short.pdf
> <http://www.cis.ksu.edu/%7Etamtoft/Papers/Amt+Ban:CondInfFlow-2007/short.pdf>
>
> --- Correctness of Practical Slicing for Modern Program Structures ---
>
> Abstract:
> Slicing is a program transformation technique with numerous
> applications, since it allows the user to focus on the parts of a
> given program that are relevant for a given purpose.  Ideally, the
> sliced program should have the same termination properties as the
> original program, but to achieve this, the slicing algorithm must
> include in the slice all commands that influence the guards of
> potential loops.  For practical purposes, so as to keep the slices
> manageable, it might be better to slice away loops that do not affect
> the values of relevant variables. The corresponding correctness
> criterion is then that the observational behavior of the original
> program is a *prefix* of the behavior of the sliced program.
>
> This paper presents foundational work that shows how to accomplish
> this goal for arbitrary control flow graphs, including those that are
> irreducible, or have zero or multiple end nodes.  This is in contrast
> to previous definitions that have made various assumptions about the
> control flow graph.  Therefore, the proposed approach is able to
> handle the control flow graphs that arise from modern program
> structures, such as when modeling reactive systems.  A correct slice
> is defined as one which is closed under data dependency and under a
> certain variant of control dependency, called "weak order dependency",
> which was recently proposed in order to handle irreducible control
> flow graphs.  These definitions allow a crisp correctness proof, based
> on simulation techniques.
>
> http://www.cis.ksu.edu/~tamtoft/Papers/Amt:WodSlicing-2007/short.pdf
> <http://www.cis.ksu.edu/%7Etamtoft/Papers/Amt:WodSlicing-2007/short.pdf>
>
>
>
-------------- next part --------------
HTML attachment scrubbed and removed