Campus Event Calendar

Event Entry

New for: D1, D3, D4, D5

What and Who

"Proving GUIs Correct: Verifying Higher-Order Imperative Programs withHigher-Order Separation Logic"

Neelakantan R. Krishnaswami
CMU Computer Science Department at Pittsburgh
SWS Colloquium
AG 1, AG 3, AG 4, AG 5, SWS, RG1, MMCI  
Expert Audience

Date, Time and Location

Monday, 20 April 2009
60 Minutes
E1 5
Wartburg OG 5


O'Hearn and Reynolds' separation logic has proven to be a very
successful attempt at taming many of the difficulties associated
with reasoning about aliased, mutable data structures. Using
it, researchers have given correctness proofs of even quite
intricate low-level imperative programs such as garbage collectors
and device drivers.

However, high level languages such as ML and Haskell also give
programmers access to mutable, aliased data, and when those features
are used, programmers are still prone to all the troubles state is
heir to. In fact, many problems become more complex, since these
languages encourage the use of an abstract, higher-order style, and
support the design of libraries that rely on higher-order functions
as well as callbacks (ie, references to functions in the heap).

In this talk, I'll describe work I've done (in collaboration with
my PhD supervisors) designing a version of separation logic suitable
for use in languages such as ML, and describe an application of this
logic to formally verifying the correctness of a small library for
writing event-driven programs in a lazy dataflow style. This then
allows an efficient imperative implementation of a functional reactive
programming library.


--email hidden

Video Broadcast

E1 4
passcode not visible
logged in users only

Bettina Peden-Bennett, 04/27/2009 13:32 -- Created document.