Local reasoning about the presence of bugs: incorrectness separation logic

DOI10.1007/978-3-030-53291-8_14zbMath1478.68057OpenAlexW3043626952MaRDI QIDQ2226739

Hoang-Hai Dang, Peter W. O'Hearn, Josh Berdine, Azalea Raad, Jules Villard, Derek R. Dreyer

Publication date: 9 February 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-53291-8_14

zbMATH Keywords

separation logicprogram logicsbug catching

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (10)

Logic for reasoning about bugs in loops over data sequences (IFIL) ⋮ Adversarial logic ⋮ Limits and difficulties in the design of under-approximation abstract domains ⋮ Property-driven code obfuscations reinterpreting Jones-optimality in abstract interpretation ⋮ Local completeness logic on Kleene algebra with tests ⋮ On algebra of program correctness and incorrectness ⋮ An adaptation-complete proof system for local reasoning about cloud storage systems ⋮ Reasoning about block-based cloud storage systems via separation logic ⋮ Monadic second-order incorrectness logic for GP 2 ⋮ Incorrectness logic for graph programs

This page was built for publication: Local reasoning about the presence of bugs: incorrectness separation logic