Incorrectness separation logic (ISL) was recently introduced as a theory of under-approximate reasoning, with the goal of proving that compositional bug catchers find actual bugs. However, ISL only considers sequential programs. Here, we develop concurrent incorrectness separation logic (CISL), which extends ISL to account for bug catching in concurrent programs. Inspired by the work on Views, we design CISL as a parametric framework, which can be instantiated for a number of bug catching scenarios, including race detection, deadlock detection, and memory safety error detection. For each instance, the CISL meta-theory ensures the soundness of incorrectness reasoning for free, thereby guaranteeing that the bugs detected are true positives.
Wed 19 JanDisplayed time zone: Eastern Time (US & Canada) change
Wed 19 Jan
Displayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00 | |||
10:20 25mTalk | A Separation Logic for Heap Space under Garbage CollectionRemote POPL DOI Media Attached | ||
10:45 25mResearch paper | Simuliris: A Separation Logic Framework for Verifying Concurrent Program OptimizationsDistinguished PaperRemote POPL Lennard Gäher MPI-SWS, Michael Sammler MPI-SWS, Simon Spies MPI-SWS, Ralf Jung MPI-SWS, Hoang-Hai Dang MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Jeehoon Kang KAIST, Derek Dreyer MPI-SWS DOI Media Attached | ||
11:10 25mResearch paper | Concurrent Incorrectness Separation LogicRemote POPL Azalea Raad Imperial College London, Josh Berdine Meta, Derek Dreyer MPI-SWS, Peter W. O'Hearn Meta; University College London DOI Media Attached | ||
11:35 25mResearch paper | On Incorrectness Logic and Kleene Algebra with Top and TestsInPerson POPL Cheng Zhang Boston University, Arthur Azevedo de Amorim Boston University, Marco Gaboardi Boston University DOI Media Attached |