This program is tentative and subject to change.
The separation logic framework Iris has been built on the premise that all assertions are \emph{stable}, meaning they unconditionally enjoy the famous \emph{frame rule}. This gives Iris—and the numerous program logics that build on it—very modular reasoning principles. But stability also comes at a cost. It excludes a core feature of the Viper verifier family, \emph{heap-dependent expression assertions}, which lift program expressions to the assertion level in order to reduce redundancy between code and specifications and better facilitate SMT-based automation.
In this paper, we bring heap-dependent expression assertions to Iris with \textbf{Daenerys}. To do so, we must first revisit the very core of Iris, extending it with a new form of \emph{unstable resources} (and adapting the frame rule accordingly). On top, we then build a program logic with heap-dependent expression assertions and lay the foundations for connecting Iris to SMT solvers. We apply Daenerys to several case studies, including some that go beyond what Viper and Iris can do individually and others that benefit from the connection to SMT.
This program is tentative and subject to change.
Thu 19 JunDisplayed time zone: Seoul change
10:30 - 12:10 | |||
10:30 20mTalk | A Hybrid Approach to Semi-automated Rust Verification PLDI Research Papers Sacha-Élie Ayoun Imperial College London, Xavier Denis ETH Zurich, Petar Maksimović Nethermind; Imperial College London, Philippa Gardner Imperial College London DOI Pre-print | ||
10:50 20mTalk | RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers PLDI Research Papers Kimaya Bedarkar Max Planck Institute for Software Systems (MPI-SWS), Laila Elbeheiry MPI-SWS, Michael Sammler ETH Zurich; ISTA, Lennard Gäher MPI-SWS, Björn Brandenburg MPI-SWS, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS DOI | ||
11:10 20mTalk | Certified Compilers à la Carte PLDI Research Papers Oghenevwogaga Ebresafe University of Waterloo, Ian Zhao University of Waterloo, Ende Jin University of Waterloo, Arthur Bright University of Waterloo, Charles Jian University of Waterloo, Yizhou Zhang University of Waterloo DOI | ||
11:30 20mTalk | Destabilizing Iris PLDI Research Papers Simon Spies MPI-SWS, Niklas Mück MPI-SWS, Haoyi Zeng Saarland University, Michael Sammler ETH Zurich; ISTA, Andrea Lattuada MPI-SWS, Peter Müller ETH Zurich, Derek Dreyer MPI-SWS DOI | ||
11:50 20mTalk | Verifying Lock-Free Traversals in Relaxed Memory Separation Logic PLDI Research Papers DOI |