Reasoning About Programs in Higher-Order Concurrent Separation Logic
Higher-order concurrent separation logic has been very successful in verifying correctness of intricate programs and reasoning about programming languages. In this talk we will present some basic ideas of program verification, separation logic, and how to use higher-order concurrent separation logic to reason about programs and programming languages. In particular, we will present and discuss the Iris program logic which is a general framework for defining separation logics and using them to reason about programs and programming languages.
Mon 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:00 - 19:30
|Reasoning About Programs in Higher-Order Concurrent Separation Logic|
Amin Timany Aarhus University
|εσόμεθα πολλώ κάρρονες – making your way in a changing world|
Sophia Drossopoulou Imperial College London