Tuesday, May 15, 2018 - 2:30pm to 3:30pm

Location:

Speaker:

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.

—

David Van Horn is an Assistant Professor at the University of Maryland, College Park where he co-directs the Programming Languages Lab (PLUM Lab).

Faculty Host: Robert Harper

For More Information, Contact:

Keywords: