2026-07-17T20:18:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12349 2024-03-06T10:50:01Z ddc:004 open_access

Symbolic Execution Game Semantics Lin, Yu-Yang Tzevelekos, Nikos game semantics symbolic execution higher-order open programs We present a framework for symbolically executing and model checking higher-order programs with external (open) methods. We focus on the client-library paradigm and in particular we aim to check libraries with respect to any definable client. We combine traditional symbolic execution techniques with operational game semantics to build a symbolic execution semantics that captures arbitrary external behaviour. We prove the symbolic semantics to be sound and complete. This yields a bounded technique by imposing bounds on the depth of recursion and callbacks. We provide an implementation of our technique in the 𝕂 framework and showcase its performance on a custom benchmark based on higher-order coding errors such as reentrancy bugs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yu-Yang Lin and Nikos Tzevelekos 2020 Is Part Of LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2020.27 urn:nbn:de:0030-drops-123493 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.27 eng https://creativecommons.org/licenses/by/3.0/legalcode