DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2020.27

Symbolic Execution Game Semantics

Authors: Yu-Yang Lin and Nikos Tzevelekos

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

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.

Cite as

Yu-Yang Lin and Nikos Tzevelekos. Symbolic Execution Game Semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 27:1-27:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{lin_et_al:LIPIcs.FSCD.2020.27,
  author =	{Lin, Yu-Yang and Tzevelekos, Nikos},
  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 =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.27},
  URN =		{urn:nbn:de:0030-drops-123493},
  doi =		{10.4230/LIPIcs.FSCD.2020.27},
  annote =	{Keywords: game semantics, symbolic execution, higher-order open programs}
}

Search Results

Documents authored by Lin, Yu-Yang

Symbolic Execution Game Semantics

Abstract

Cite as

Thanks for your feedback!

Could not send message