Aarhus University Seal / Aarhus Universitets segl

LS Talk: Modular reasoning for modular concurrency, Aaron Turon

Logic and Semantics Talk

Info about event


Thursday 18 April 2013,  at 13:00 - 14:00


INCUBA-112, Åbogade 15, 8200 Aarhus N


Lars Birkedal


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



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.