Symbolic Execution Game Semantics

TL;DR

This paper introduces a novel symbolic execution framework for higher-order programs that integrates game semantics to accurately model external behaviors, enabling effective verification of client-library interactions.

Contribution

It combines symbolic execution with game semantics to handle external methods, providing a sound and complete bounded analysis technique for higher-order programs.

Findings

Implemented in the K framework for practical use.

Successfully detected higher-order coding errors like reentrancy bugs.

Demonstrated effectiveness on custom benchmarks.

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 K framework and showcase its performance on a custom benchmark based on higher-order coding errors such as reentrancy bugs.