[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

NU Programming Languages Seminar
Wed, 5/30/07
11:45am-1:30pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Torben Amtoft
Kansas State University

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


Upcoming Events:

# 6/1 "Conversations with Functional Programmers" @ Harvard
# Don't you want to speak at pl-seminar?

--Mitch