Bounded Verification of Higher-Order Stateful Programs

In this thesis we explore bounded verification techniques for higher-order stateful programs. We consider two settings: open and closed higher-order, which are defined by the type-order of free variables present in each. Closed higher-order programs allow free variables only if they are of ground type, whereas open higher-order programs generalise this by allowing free variables of arbitrary order. We elaborate on the challenges involved in reasoning within said settings, and define a higher-order stateful language—an ML-like -calculus with recursion and higher-order global state—as our vehicle of study. We define a Bounded Model Checking technique for closed higher-order programs via defunctionalization using nominal techniques, and a Symbolic Execution Game Semantics to perform Bounded Symbolic Execution of open higher-order programs. Contributions presented in this thesis involve theoretical and experimental results. On the theoretical side, all approaches defined herein are sound and bounded-complete in the sense that they report errors if and only if errors are reachable up to the given bound—all results necessary to show this are included. For the experimental side, we implemented prototype tools for each technique, collected and created benchmarks to test each higher-order setting, and measured the performance of our tools to compare them to other relevant existing tools. Results presented herein for closed and open higher-order programs have been published in SETTA 2019 and FSCD 2020 respectively