Principals of Programming Seminar - Postponed
— 3:30pm
Location:
Traffic21 Classroom 6501
-
Gates Hillman Centers
Speaker:
DAVID VAN HORN - Postponed
,
Assistant Professor, Department of Computer Science
https://www.cs.umd.edu/~dvanhorn/
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:
bcook@cs.cmu.edu