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
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 20 April 2009
13:30
60 Minutes
E1 5
Wartburg OG 5
Saarbrücken
Abstract
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.
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.
Contact
--email hidden
Video Broadcast
Yes
Saarbrücken
E1 4
019
passcode not visible
logged in users only
Bettina Peden-Bennett, 04/27/2009 13:32 -- Created document.