DARTS.10.2.13.pdf
- Filesize: 392 kB
- 2 pages
Document
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact)
Authors
-
Part of:
Issue:
Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Volume: DARTS, Volume 10 (ECOOP 2024)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-09-12
Artifact Description
Document Identifiers
Acknowledgements
We would like José Fragoso Santos for producing the original version of Gillian. We would also like to thank the anonymous reviewers for their comments.
Cite AsGet BibTex
Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Nat Karmios, Petar Maksimović, and Philippa Gardner. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 13:1-13:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/DARTS.10.2.13
https://doi.org/10.4230/DARTS.10.2.13
Artifact
DARTS-10-2-13-artifact-0b18868dfa3cdeeebadefa7fd3266057.zip
(Filesize: 9.83 GB)
Artifact Evaluation Policy
The artifact has been evaluated as described in the ECOOP 2024 Call for Artifacts and the ACM Artifact Review and Badging Policy.
Abstract
This artifact is a companion to the paper "Compositional Symbolic Execution for Correctness and Incorrectness Reasoning". It contains the source code of the Gillian compositional symbolic execution (CSE) platform, in which we added the incorrectness reasoning capabilities, and the benchmarks used in the evaluation of the paper. It also contains a Haskell demonstrator CSE engine that directly implements the CSE engine inference rules presented in the paper.
Subject Classification
ACM Subject Classification
- Theory of computation → Program verification
- Theory of computation → Program analysis
- Theory of computation → Separation logic
- Theory of computation → Automated reasoning
Keywords
- separation logic
- incorrectness logic
- symbolic execution
- bi-abduction
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads