Distinguished Paper Award at CPP 2025
We are happy to announce that the research paper ‘The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic’ has received the CPP 2025 Distinguished Paper Award.
Written by PhD students Simon Friis Vindum (now at GitHub), Aina Linn Georges (now postdoc at Max Planck Institute for Software Systems), and Professor Lars Birkedal, the paper introduces the nextgen modality, a groundbreaking contribution to separation logic. By enabling reasoning across generations with non-local and non-frame-preserving updates, this work pushes the boundaries of program reasoning and enriches the Iris base logic.
Read the full paper here at️ https://cs.au.dk/~birke/papers/index.html
This prestigious recognition highlights the significant impact of their research in advancing the theoretical and practical foundations of formal verification and certification.
Certified Programs and Proofs (CPP) is a leading international conference exploring formal verification and certification across computer science, mathematics, logic, and education. Co-located with POPL 2025, CPP 2025 takes place this January in Denver, Colorado, USA.