PhD Proposal: Higher-order Symbolic Execution

Expressive programming language features pose significant challenges for static verification. First-class functions prevent program flows from being straightforwardly computed from syntax. Dynamic typing obscures basic invariants about data shapes, which is only worsened by dynamic typing idioms that rely on path-sensitive, interprocedural reasoning to justify the use of partial functions. Mutable states introduce implicit communication channels that can invalidate previously established invariants. Control operators destroy assumptions about “well-bracketed” program flows. The interaction of these features only introduce more opportunities for unexpected behavior, challenging manual as well as automatic reasoning.The lack of effective static verification for expressive programming languages means programmers have to resort to run-time checks and extensive test suites in order to provide reasonable guarantees about their program’s correctness. Resorting to pure run-time checks is sub-optimal: it delays error discovery and introduces significant overhead. Testing alone cannot prove the absence of errors, and large test suites cannot provide instant feedback.This seeming trade-off between a programming language’s expressiveness and its analyzability needs not be a reality. Higher-order symbolic execution is a novel framework for deriving sound, precise, and scalable static verification for expressive programming languages. Finitized symbolic execution can be viewed as verification, where dynamic checks are the specifications, and the lack of run-time errors signifies correctness. Soundness in the presence of symbolic functions is defined and proven by employing the blame semantics from work on higher-order contracts. To demonstrate reproducible bugs to programmers, a refinement to symbolic execution yields an analysis that can also generate concrete, potentially higher-order counterexamples. We can prove that symbolic functions do not fundamentally make counterexample generation more difficult, and the search is relatively complete with respect to the underlying first-order SMT solver. A further extension to the rule for symbolic function application yields a verifier that can soundly handle higher-order imperative programs with challenging patterns such as higher-order stateful call-backs and aliases to mutable states. In all cases, the verification is modular, in the sense that components can be omitted in place of their specifications. In addition, unverifiable programs due to the inherent limitation of static analysis can still be run with residual dynamic checks. In the end, the verification allows programmers to benefit from static verification as much as possible without compromising language features that may not fit in any particular static discipline. An extension to this work will be turning the existing contract verifier into a theorem prover, an important mile-stone of which is reformulating termination as a dynamically checkable property.

Examining Committee:

Chair: Dr. David Van Horn Dept. rep: Dr. Dinesh Manocha Members: Dr. Michael Hicks