Concurrent incorrectness separation logic

File Description SizeFormat 
3498695.pdfPublished version864.05 kBAdobe PDFView/Open
Title: Concurrent incorrectness separation logic
Authors: Raad, A
Berdine, J
Dreyer, D
O'Hearn, PW
Item Type: Journal Article
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.
Issue Date: 16-Jan-2022
Date of Acceptance: 1-Jan-2022
URI: http://hdl.handle.net/10044/1/97422
DOI: 10.1145/3498695
ISSN: 2475-1421
Publisher: Association for Computing Machinery (ACM)
Start Page: 1
End Page: 29
Journal / Book Title: Proceedings of the ACM on Programming Languages
Volume: 6
Issue: POPL
Copyright Statement: © 2022 Copyright held by the owner/author(s).
Sponsor/Funder: UK Research and Innovation
Funder's Grant Number: MR/V024299/1
Publication Status: Published
Open Access location: https://dl.acm.org/doi/10.1145/3498695
Online Publication Date: 2022-01-16
Appears in Collections:Computing



This item is licensed under a Creative Commons License Creative Commons