A general approach to under-approximate reasoning about concurrent programs

DOI10.4230/LIPICS.CONCUR.2023.25MaRDI QIDQ6967322zbMATH OpenFDO

Authors Azalea Raad, Julien Vanegue, Josh Berdine, Peter W. O'Hearn

Publication date 26 June 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.CONCUR.2023.25

zbMATH Keywords

bug detectionincorrectness logicseparation logicsoftware exploitsunder-approximate reasoning

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites work

• A Marriage of Rely/Guarantee and Separation Logic
• CONCUR 2004 - Concurrency Theory
• Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
• Local reasoning about the presence of bugs: incorrectness separation logic
• Tentative steps toward a development method for interfering programs

This page was built for publication: A general approach to under-approximate reasoning about concurrent programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6967322)