[Pl-seminar] Semantics Seminar Schedule

Mitchell Wand wand at ccs.neu.edu
Sat May 26 00:05:10 EDT 2007

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

Torben Amtoft
Kansas State University

Verification Condition Generation for Conditional Information Flow


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.

Upcoming Events:

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


More information about the pl-seminar mailing list