Higher-order Symbolic Execution

Abstract

There are multiple challenges in designing a static verification system for an existing programming language. There is the technical challenge of achieving soundness and precision in the presence of expressive language features such as dynamic typing, higher-order functions, mutable state, control operators, and their idiomatic usage. There is also the practical challenge of allowing gradual adoption of verification in the face of large code bases in the real world. Failure to achieve this gradual property hinders the system’s adoption in practice: Existing correct but unverifiable components due to the lack of annotations, the unavailability or the source code, or the inherent incompleteness of static checking would require tedious modifications to a program to make it safe and executable again.

This dissertation shows a simple framework for integrating rich static reasoning into an existing expressive programming language by leveraging dynamic checks and a novel form of symbolic execution. Higher-order symbolic execution enables gradual verification that is sound, precise, and modular for expressive programming languages. First, symbolic execution can be generalized to higher-orderprogramming languages: Symbolic functions do not make bug-finding and counterexample generation fundamentally more difficult, and the counterexample search is relatively complete with respect to the underlying first-order SMT solver. Next, finitized symbolic execution can be viewed as verification, where dynamic contracts are the specifications, and the lack of run-time errors signifies correctness. A further refinement to the semantics of applying symbolic functions yields a verifier that soundly handles higher-order imperative programs with challenging patterns such as higher-order stateful call-backs and aliases to mutable state. Finally, with a novel formulation of termination as a run-time contract, symbolic execution can also verify total-correctness.

Using symbolic execution to statically verify dynamic checks has important consequences in scaling the tool in practice. Because symbolic execution closely models the standard semantics, dynamic language features and idioms such as first-class contracts and run-time type tests do not introduce new challenges to verification and bug-finding. Moreover, the method allows gradual addition and strengthening of specifications into an existing program without requiring a global re-factorization: The programmer can decide to stop adding contracts at any point and still have an executable and safe program. Properties that are unverifiable statically can be left as residual checks with the existing familiar semantics. Programmers benefit from static verification as much as possible without compromising language features that may not fit in a particular static discipline. In particular, this dissertation lays out the path to adding gradual theorem proving into an existing untyped, higher-order, imperative programming language.