Document Open Access Logo

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact)

Authors Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Nat Karmios, Petar Maksimović, Philippa Gardner

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.10.2.13.pdf
  • Filesize: 392 kB
  • 2 pages

Document Identifiers

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get 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

Author Details

Andreas Lööw
  • Imperial College London, UK
Daniele Nantes-Sobrinho
  • Imperial College London, UK
Sacha-Élie Ayoun
  • Imperial College London, UK
Caroline Cronjäger
  • Ruhr-Universität Bochum, Germany
Nat Karmios
  • Imperial College London, UK
Petar Maksimović
  • Imperial College London, UK
  • Runtime Verification Inc., Chicago, IL, USA
Philippa Gardner
  • Imperial College London, UK

Funding

This work was supported by the EPSRC Fellowship “VetSpec: Verified Trustworthy Software Specification” (EP/R034567/1).

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.

Artifact

  MD5 Sum: 0b18868dfa3cdeeebadefa7fd3266057 (Get MD5 Sum)

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.

Related Article

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact