Raad, A;
Berdine, J;
Dreyer, D;
O'Hearn, PW;
(2022)
Concurrent incorrectness separation logic.
Proceedings of the ACM on Programming Languages
, 6
(POPL)
34:1-34:29.
10.1145/3498695.
Preview |
Text
3498695.pdf - Published Version Download (487kB) | Preview |
Abstract
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.
| Type: | Article |
|---|---|
| Title: | Concurrent incorrectness separation logic |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1145/3498695 |
| Publisher version: | https://doi.org/10.1145/3498695 |
| Language: | English |
| Additional information: | This work is licensed under a Creative Commons Attribution 4.0 International License. |
| Keywords: | Concurrency, program logics, separation logic, bug catching |
| UCL classification: | UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science UCL > Provost and Vice Provost Offices > UCL BEAMS UCL |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10143247 |
Loading...
Loading...Loading...Loading...Archive Staff Only
 |
View Item |
