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 states, control operators, and their idiomatic usage. There is also the practical challenge of allowing gradual adoption of the verification in the face of large code bases in the real world. Failure to achieve this gradual property hinders the system’s adoption in multiple ways. First, correct but unverifiable components due to the inherent incompleteness of static checking would prevent some safe programs from being run. Second, the source code of all program components would need to be available, and the entire program would need to be annotated in order to be safe and executable again.

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.

 

                          Chair:               Dr. David Van Horn
                          Dean's rep:      Dr. Tudor Dumitras
                          Members:        Dr. Michael Hicks
                                                    Dr. Rance Cleaveland
                                               Dr. Sam Tobin-Hochstadt