License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2023.9
URN: urn:nbn:de:0030-drops-190035
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/19003/
Kløvstad, Åsmund Aqissiaq Arild ;
Kamburjan, Eduard ;
Johnsen, Einar Broch
Compositional Correctness and Completeness for Symbolic Partial Order Reduction
Abstract
Partial Order Reduction (POR) and Symbolic Execution (SE) are two fundamental abstraction techniques in program analysis. SE is particularly useful as a state abstraction technique for sequential programs, while POR addresses equivalent interleavings in the execution of concurrent programs. Recently, several promising connections between these two approaches have been investigated, which result in symbolic partial order reduction: partial order reduction of symbolically executed programs. In this work, we provide compositional notions of completeness and correctness for symbolic partial order reduction. We formalize completeness and correctness for (1) abstraction over program states and (2) trace equivalence, such that the abstraction gives rise to a complete and correct SE, the trace equivalence gives rise to a complete and correct POR, and their combination results in complete and correct symbolic partial order reduction. We develop our results for a core parallel imperative programming language and mechanize the proofs in Coq.
BibTeX - Entry
@InProceedings{klovstad_et_al:LIPIcs.CONCUR.2023.9,
author = {Kl{\o}vstad, \r{A}smund Aqissiaq Arild and Kamburjan, Eduard and Johnsen, Einar Broch},
title = {{Compositional Correctness and Completeness for Symbolic Partial Order Reduction}},
booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)},
pages = {9:1--9:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-299-0},
ISSN = {1868-8969},
year = {2023},
volume = {279},
editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/19003},
URN = {urn:nbn:de:0030-drops-190035},
doi = {10.4230/LIPIcs.CONCUR.2023.9},
annote = {Keywords: Symbolic Execution, Coq, Trace Semantics, Partial Order Reduction}
}
Keywords: |
|
Symbolic Execution, Coq, Trace Semantics, Partial Order Reduction |
Collection: |
|
34th International Conference on Concurrency Theory (CONCUR 2023) |
Issue Date: |
|
2023 |
Date of publication: |
|
07.09.2023 |
Supplementary Material: |
|
Software (Coq proofs): https://doi.org/10.5281/zenodo.8070170 |