David van Horn
Symbolic Execution for Higher-Order Program Verification
April 24, 2018 at 12:00pm (lunch talk) CSE 305
Abstract
In this talk, I will describe recent work on automatically verifying programs written in higher-order and imperative program languages using a novel form of symbolic execution.
Our approach to higher-order symbolic execution is sound and relatively complete with respect to a first-order solver for base-type values. I’ll show that the approach (1) is competitive with a range of program verification techniques including type systems, flow analyzers, and model checkers, (2) can often generate counter-examples, even higher-order ones, when verification fails, and (3) can be used to effectively verify either complete or partial contract correctness of components written in an untyped, higher-order and imperative language with first-class contracts, where, as a consequence of soundness, we can establish a theorem guaranteeing that verified components can’t be blamed.
More broadly, I will draw connections between this work and two areas of earlier work I’ve done on the computational complexity of program analysis problems and a systematic approach to abstract interpretation (called Abstracting Abstract Machines). Finally, I will sketch how this work connects to other areas in interactive program verification, incremental computation, gradual type systems, and termination analysis.
This talk will assume a basic familiarity with functional programming and graduate-level exposure to PL semantics, in particular reduction semantics. No background in program analysis or abstract interpretation is necessary.
Bio
David Van Horn is an Assistant Professor at the University of Maryland, College Park where he co-directs the PLUM Lab.