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{Le:2022:10.1145/3527325,
author = {Le, QL and Raad, A and Villard, J and Berdine, J and Dreyer, D and O'Hearn, PW},
doi = {10.1145/3527325},
journal = {Proceedings of the ACM on Programming Languages},
pages = {1--27},
title = {Finding real bugs in big programs with incorrectness logic},
url = {http://dx.doi.org/10.1145/3527325},
volume = {6},
year = {2022}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - Incorrectness Logic (IL) has recently been advanced as a logical theory for compositionally proving the presence of bugs—dual to Hoare Logic, which is used to compositionally prove their absence. Though IL was motivated in large part by the aim of providing a logical foundation for bug-catching program analyses, it has remained an open question: is IL useful only retrospectively (to explain existing analyses), or can it actually be useful in developing new analyses which can catch real bugs in big programs?In this work, we develop Pulse-X, a new, automatic program analysis for catching memory errors, based on ISL, a recent synthesis of IL and separation logic. Using Pulse-X, we have found 15 new real bugs in OpenSSL, which we have reported to OpenSSL maintainers and have since been fixed. In order not to be overwhelmed with potential but false error reports, we develop a compositional bug-reporting criterion based on a distinction between latent and manifest errors, which references the under-approximate ISL abstractions computed by Pulse-X, and we investigate the fix rate resulting from application of this criterion. Finally, to probe the potential practicality of our bug-finding method, we conduct a comparison to Infer, a widely used analyzer which has proven useful in industrial engineering practice.
AU  - Le,QL
AU  - Raad,A
AU  - Villard,J
AU  - Berdine,J
AU  - Dreyer,D
AU  - O'Hearn,PW
DO  - 10.1145/3527325
EP  - 27
PY  - 2022///
SN  - 2475-1421
SP  - 1
TI  - Finding real bugs in big programs with incorrectness logic
T2  - Proceedings of the ACM on Programming Languages
UR  - http://dx.doi.org/10.1145/3527325
UR  - https://dl.acm.org/doi/10.1145/3527325
UR  - http://hdl.handle.net/10044/1/97408
VL  - 6
ER  -
Download