Principals of Programming Seminar - Postponed

Tuesday, May 15, 2018 - 2:30pm to 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, Contact:

Keywords:

Seminar Series

Undergraduate Programs

The admissions process for each undergraduate major varies from program to program, but admissions for our main bachelor of science in computer science are handled through Carnegie Mellon's central Office of Undergraduate Admission. Learn more on our Undergraduate Admissions page.

Master's Programs

The Computer Science Department offers a main M.S. in Computer Science, and applications for that program are submitted online by mid-December for fall admission the following year. Other master's programs available to CSD students have their own admissions processes. Learn more about our admissions requirements and processes here.

Doctoral Programs

The Ph.D. in CS program uses the School of Computer Science online application for admissions. Applications are due in December for admittance the following fall. Students cannot begin in the spring. For more on how to apply, visit our Doctoral Admissions page.

Apply

Faculty Positions

The 2017-2018 application period for the Computer Science Department (CSD) at Carnegie Mellon University has closed for positions starting in Fall 2018.

Each year we seek candidates who have demonstrated commitment to excellence and leadership in undergraduate and graduate teaching, research, and/or service toward building an equitable and diverse scholarly environment.

Additional information can be found on our Faculty Hiring page. Please check back in September for the next hiring period for positions starting in Fall 2019.