License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2020.27
URN: urn:nbn:de:0030-drops-123493
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12349/
Go to the corresponding LIPIcs Volume Portal

Lin, Yu-Yang ; Tzevelekos, Nikos

Symbolic Execution Game Semantics

pdf-format:
LIPIcs-FSCD-2020-27.pdf (0.7 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{lin_et_al:LIPIcs:2020:12349,
  author =	{Yu-Yang Lin and Nikos Tzevelekos},
  title =	{{Symbolic Execution Game Semantics}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{27:1--27:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Zena M. Ariola},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12349},
  URN =		{urn:nbn:de:0030-drops-123493},
  doi =		{10.4230/LIPIcs.FSCD.2020.27},
  annote =	{Keywords: game semantics, symbolic execution, higher-order open programs}
}

Keywords: game semantics, symbolic execution, higher-order open programs
Collection: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Issue Date: 2020
Date of publication: 28.06.2020
Supplementary Material: The tool and its benchmarks can be found at: https://github.com/LaifsV1/HOLiK.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI