ECOOP 2025 (series) / FTfJP 2025 (series) / FTfJP 2025 – Formal Techniques for Judicious Programming /
Towards a Unifying Semantics Playground
We give a brief presentation of how Unifying Theories of Programming (UTP) can be used to define program languages and their semantics. We describe and show examples of the use of a prototype theorem-prover reasonEq that supports equational reasoning for UTP. We discuss how this tool is intended to support work into various formal approaches to concurrency.
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 | ||