[Pl-seminar] 9/30: Zachary Kincaid, Proof Spaces for Unbounded Parallelism

[Vincent St-Amour]

NUPRL Seminar presents

Zachary Kincaid
University of Toronto

11:00 - 12:30
Tuesday, 9/30
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)


Proof Spaces for Unbounded Parallelism

Abstract:
One of the main challenges of algorithmic software verification is
coping with the infinite: a program has (potentially) infinitely many
states, and a program verifier must prove that each one of them
satisfies some property in a finite amount of time. Multi-threading
introduces a new source of infinity: not only does each thread have
infinitely many states, but there are infinitely many threads running
simultaneously and interacting with one another. In this talk, I'll
describe proof spaces, a proof system for multi-threaded programs. Proof
spaces allow automated program verifiers to divide the labour of
reasoning about the two sources of infinity, tackling each of them
separately but in a way that does not sacrifice reasoning power. I will
discuss the expressiveness of proof spaces and the algorithms involved
in automating them.


------------------------------------------------------------------------------

Also, an announcement:

Thanks for filling out our scheduling poll! This semester, talks will be
held on Fridays from 1:30 to 3:00 (the above talk being an exception).