Principals of Programming Seminar - Postponed May 15, 2018 2:30pm — 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 Add event to Google Add event to iCal