Local reasoning about the presence of bugs: incorrectness separation logic
From MaRDI portal
Publication:2226739
DOI10.1007/978-3-030-53291-8_14zbMath1478.68057MaRDI 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
03B70: Logic in computer science
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
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, 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, On algebra of program correctness and incorrectness