[Pl-seminar] TIME CHANGE: 12:30--14:00, for 1/14 Seminar: Viktor Vafeiadis, Program verification under weak memory consistency

[William J. Bowman]

Time change: the talk is now 12:30--14:00.

I apologize for the inconvenience.

--
William J. Bowman

On Fri, Jan 08, 2016 at 04:02:26PM -0500, William J. Bowman wrote:
> NUPRL Seminar presents
> 
> Viktor Vafeiadis
> Max Planck Institute for Software Systems
> 
> <s>13:30--15:00</s>12:30--14:00
> Thursday, Jan. 14, 2016
> Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
> Host: Amal Ahmed
> 
> 
> Program verification under weak memory consistency
> 
> Abstract:
> Weak memory models formalize the inconsistent behaviors that one can
> observe in multithreaded programs running on modern hardware.
> In so doing, they complicate the already-difficult task of reasoning
> about correctness of concurrent code.
> Worse, they render impotent most formal methods that have been
> developed to tame concurrency, which almost universally assume a
> strong (i.e., sequentially consistent) memory model.
> In response, we have developed a number of alternative reasoning
> techniques that are sound for programs running weak memory
> consistency.
> I will cover both program logics, such as relaxed separation logic, as
> well as theorems that allow reducing reasoning about well-structured
> weakly consistent implementations down to sequential consistency, and
> show how these can be applied to reason about a practical RCU
> implementation.
> 
> 
> Bio:
> Viktor Vafeiadis is a tenure-track researcher at MPI-SWS.
> He received his BA (2004) and PhD (2008) from the University of
> Cambridge.
> Before joining MPI-SWS in October 2010, he was a postdoc at Microsoft
> Research and at the University of Cambridge.
> He is interested in programming languages and verification with a
> focus program logics for weak memory, program logics for concurrency,
> compiler verifications, automated verification of concurrent programs,
> and interactive theorem proving.
> 
> -- 
> William J. Bowman
> Northeastern University
> College of Computer and Information Science



> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: not available
URL: <http://lists.ccs.neu.edu/pipermail/pl-seminar/attachments/20160112/921eb181/attachment.pgp>