Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic

There has been a large body of work on local reasoning for proving the absence of bugs, but none for proving their presence. We present a new formal framework for local reasoning about the presence of bugs, building on two complementary foundations: 1) separation logic and 2) incorrectness logic. We...

Descripción completa

Detalles Bibliográficos
Autores principales: Raad, Azalea, Berdine, Josh, Dang, Hoang-Hai, Dreyer, Derek, O’Hearn, Peter, Villard, Jules
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363320/
http://dx.doi.org/10.1007/978-3-030-53291-8_14
_version_ 1783559642997063680
author Raad, Azalea
Berdine, Josh
Dang, Hoang-Hai
Dreyer, Derek
O’Hearn, Peter
Villard, Jules
author_facet Raad, Azalea
Berdine, Josh
Dang, Hoang-Hai
Dreyer, Derek
O’Hearn, Peter
Villard, Jules
author_sort Raad, Azalea
collection PubMed
description There has been a large body of work on local reasoning for proving the absence of bugs, but none for proving their presence. We present a new formal framework for local reasoning about the presence of bugs, building on two complementary foundations: 1) separation logic and 2) incorrectness logic. We explore the theory of this new incorrectness separation logic (ISL), and use it to derive a begin-anywhere, intra-procedural symbolic execution analysis that has no false positives by construction. In so doing, we take a step towards transferring modular, scalable techniques from the world of program verification to bug catching.
format Online
Article
Text
id pubmed-7363320
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73633202020-07-16 Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic Raad, Azalea Berdine, Josh Dang, Hoang-Hai Dreyer, Derek O’Hearn, Peter Villard, Jules Computer Aided Verification Article There has been a large body of work on local reasoning for proving the absence of bugs, but none for proving their presence. We present a new formal framework for local reasoning about the presence of bugs, building on two complementary foundations: 1) separation logic and 2) incorrectness logic. We explore the theory of this new incorrectness separation logic (ISL), and use it to derive a begin-anywhere, intra-procedural symbolic execution analysis that has no false positives by construction. In so doing, we take a step towards transferring modular, scalable techniques from the world of program verification to bug catching. 2020-06-16 /pmc/articles/PMC7363320/ http://dx.doi.org/10.1007/978-3-030-53291-8_14 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Raad, Azalea
Berdine, Josh
Dang, Hoang-Hai
Dreyer, Derek
O’Hearn, Peter
Villard, Jules
Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic
title Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic
title_full Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic
title_fullStr Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic
title_full_unstemmed Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic
title_short Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic
title_sort local reasoning about the presence of bugs: incorrectness separation logic
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363320/
http://dx.doi.org/10.1007/978-3-030-53291-8_14
work_keys_str_mv AT raadazalea localreasoningaboutthepresenceofbugsincorrectnessseparationlogic
AT berdinejosh localreasoningaboutthepresenceofbugsincorrectnessseparationlogic
AT danghoanghai localreasoningaboutthepresenceofbugsincorrectnessseparationlogic
AT dreyerderek localreasoningaboutthepresenceofbugsincorrectnessseparationlogic
AT ohearnpeter localreasoningaboutthepresenceofbugsincorrectnessseparationlogic
AT villardjules localreasoningaboutthepresenceofbugsincorrectnessseparationlogic

Ejemplares similares