[Pl-seminar] Semantics Seminar Schedule
wand at ccs.neu.edu
Sat May 26 00:05:10 EDT 2007
NU Programming Languages Seminar
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
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.
# 6/1 "Conversations with Functional Programmers" @ Harvard
# Don't you want to speak at pl-seminar?
More information about the pl-seminar