2026-08-01T09:54:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20911 2024-09-12T05:53:12Z ddc:004 open_access

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact) Lööw, Andreas Nantes-Sobrinho, Daniele Ayoun, Sacha-Élie Cronjäger, Caroline Karmios, Nat Maksimović, Petar Gardner, Philippa separation logic incorrectness logic symbolic execution bi-abduction 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andreas Lööw and Daniele Nantes-Sobrinho and Sacha-Élie Ayoun and Caroline Cronjäger and Nat Karmios and Petar Maksimović and Philippa Gardner 2024 Is Part Of DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DARTS.10.2.13 urn:nbn:de:0030-drops-209110 https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.13 eng https://creativecommons.org/licenses/by/4.0/legalcode