Write a Blog >>
Tue 20 Jun 2017 11:20 - 12:30 at Vertex WS217 - B Chair(s): Santosh Nagarakatte

Iris is a generic framework for higher-order concurrent separation logic, which supports the derivation of a wide variety of advanced program logics for a range of different programming languages and comes equipped with strong tactic support for proving concurrent programs correct in the Coq proof assistant (http://iris-project.org/). Although originating in 2013 from the ashes of a failed book-writing project between me and Lars Birkedal, Iris has since morphed into a serious development platform for multiple ongoing research efforts in interactive program verification. In this talk, I will give a tutorial introduction to some of the key ideas in Iris, offer some historical context about how Iris has evolved over time, and briefly describe some of the many projects that are currently using Iris to get stuff done.

This is joint work with Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Hoang-Hai Dang, Jan-Oliver Kaiser, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Amin Timany, Zhen Zhang, and Lars Birkedal.

Tue 20 Jun
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:00 - 12:30: BFTfJP at Vertex WS217
Chair(s): Santosh NagarakatteRutgers University, USA
11:00 - 11:20
A Coq-based synthesis of Scala programs which are correct-by-construction
Youssef El BakounyCIMTI - ESIB - Saint-Joseph University - Beirut, Lebanon, Tristan CrolardCEDRIC - CNAM - Paris, France, Dani MezherCIMTI - ESIB - Saint-Joseph University - Beirut, Lebanon
11:20 - 12:30
Iris: A Modular Foundation for Higher-Order Concurrent Separation Logic (KEYNOTE)