This dissertation shows a simple formula 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 is effective for deriving sound, precise, modular, and gradual verification. First, symbolic execution can be generalized to higher-order programming languages: That symbolic values also stand for functions does not make bug-finding and counterexample generation fundamentally more difficult. The search for counterexamples 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 states. Finally, with a novel formulation of termination as a run-time contract, symbolic execution can also be used to verify total-correctness.
Using symbolic execution to statically verify dynamic checks has important consequences in scaling the tool in practice. First, 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. Second, the method allows gradual addition and strengthening of specifications into an existing program without requiring a global refactorization: The programmer can decide to stop adding contracts at any point and still have an executable and safe program. Properties that cannot be statically verified due to the inherent limitation of static checking 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 toadding gradual theorem proving into an existing untyped, higher-order, imperative programming language.
Dean's rep: Dr. Tudor Dumitras
Members: Dr. Michael Hicks
Dr. Rance Cleaveland
Dr. Sam Tobin-Hochstadt
Phil Nguyen is a PhD student in the PLUM lab in the Department of Computer Science at the University of Maryland, College Park. His research interest lies in programming language semantics, verification, and meta-programming.