Imperial College London
Portrait Picture

DrAzaleaRaad

Faculty of Engineering, Department of Computing

Senior Lecturer
 
 
 
//

Contact

 

+44 (0)20 7594 8271azalea.raad Website

 
 
//

Location

 

426Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Raad:2022:10.1145/3498695,
author = {Raad, A and Berdine, J and Dreyer, D and O'Hearn, PW},
doi = {10.1145/3498695},
journal = {Proceedings of the ACM on Programming Languages},
pages = {1--29},
title = {Concurrent incorrectness separation logic},
url = {http://dx.doi.org/10.1145/3498695},
volume = {6},
year = {2022}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - 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.
AU  - Raad,A
AU  - Berdine,J
AU  - Dreyer,D
AU  - O'Hearn,PW
DO  - 10.1145/3498695
EP  - 29
PY  - 2022///
SN  - 2475-1421
SP  - 1
TI  - Concurrent incorrectness separation logic
T2  - Proceedings of the ACM on Programming Languages
UR  - http://dx.doi.org/10.1145/3498695
UR  - https://dl.acm.org/doi/10.1145/3498695
UR  - http://hdl.handle.net/10044/1/97422
VL  - 6
ER  -
Download