Speaker: Aaron Turon, http://www.mpi-sws.org/~turon/
Host: Lars Birkedal

Abstract:

Modular programming and modular verification go hand in hand, but most existing logics for concurrency ignore two crucial forms of modularity: "higher-order functions", which are essential for building reusable components, and "granularity abstraction", a key technique for hiding the intricacies of fine-grained concurrent data structures from their clients. This talk will present CaReSL, the first logic to apply granularity abstraction for modular verification of higher-order concurrent programs.  The talk is organized around a few simple but subtle examples that motivate CaReSL's key ideas, and that ultimately come together in a significant case study: the first formal proof of correctness for Hendler et al.'s "flat combining" algorithm.