[talks] A Hobor preFPO

[Melissa M Lawson]

Aquinas Hobor will present his preFPO Thursday September 20 at 10AM in room 402. 
The members of his committee are:  Advisor Andrew Appel, Readers 
David Walker, Peter O'Hearn (Queen Mary College, University of London)
Non-Readers: Vivek Pai, Brian Kernighan.  Everyone is invited to attend his talk.
His abstract follows below.


Title: "Oracle Semantics for Concurrent Separation Logic"

Abstract:

<<<

I present a model for a generalized Concurrent Separation Logic with first-class locks and
threads, and prove its soundness with respect to the operational semantics of Concurrent C
minor, a language with shared memory, spawnable threads, and sufficient expressive power
to be the target of a C, Java, or ML compiler. The model is modular in the sense that one
can reason about sequential features knowing almost nothing about concurrency, and
concurrent features knowing almost nothing about sequential control flow.
There are
substantial, but at this point incomplete, proofs of the correctness of the system in Coq.
Using the modularity principle it should be relatively straightforward to generalize
Leroy's proof of C minor compiler correctness to the concurrent case without becoming
deeply entangled in the issues of concurrency. Thus we will obtain end-to-end proofs: the
properties you prove in Concurrent Separation Logic will be true of the program that
actually executes on the machine.

>>>

Thanks,

Aquinas