ECOOP 2025 (series) / FTfJP 2025 (series) / FTfJP 2025 – Formal Techniques for Judicious Programming /
VeriFast’s separation logic: a higher-order(ish) logic without laters for modular verification of fine-grained concurrent programs
VeriFast is one of the leading tools for semi-automated modular formal program verification. A central feature of VeriFast is its support for \emph{higher-order ghost code}, which enables its support for expressively specifying fine-grained concurrent modules, without the need for a \emph{later} modality. We present the first formalization and soundness proof for this aspect of VeriFast’s logic.
Associate professor at the DistriNet research group at the Department of Computer Science, KU Leuven, Belgium
Thu 3 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Thu 3 Jul
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:45 | |||
14:00 30mTalk | From LTL to MLTL: Exploring translation between temporal logic representations using FRET and WEST FTfJP Songyan Lai Department of Computer Science, Maynooth University, Rosemary Monahan Department of Computer Science & Hamilton Institute, Maynooth University | ||
14:30 30mTalk | Towards a Unifying Semantics Playground FTfJP Andrew Butterfield Trinity College Dublin | ||
15:00 30mTalk | Towards an Axiomitisation of Solidity Memory and Storage FTfJP Guilherme Horta Alvares Da Silva Chalmers University of Technology and University of Gothenburg, Wolfgang Ahrendt Chalmers University of Technology, Richard Bubel Technische Universität Darmstadt | ||
15:30 30mTalk | VeriFast’s separation logic: a higher-order(ish) logic without laters for modular verification of fine-grained concurrent programs FTfJP Bart Jacobs DistriNet, Dept. CS, KU Leuven | ||
