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

[Vincent St-Amour]

Just a reminder: Zachary is speaking tomorrow.

Vincent



At Tue, 16 Sep 2014 14:50:14 -0400,
Vincent St-Amour wrote:
> 
> 
> 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).
> 
> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar