CAM Colloquium - Andrew Appel, Department of Computer Science, Princeton University

Formal machine-checked program verification uses mechanized logical tools to connect low-level programs to specifications of the algorithms they are supposed to implement.  The same program verification tools can work in many application domains.  But it's not enough just to implement an algorithm; the program is fully "correct" only if the algorithm (provably) computes an answer to the problem or question of interest.  Proofs of algorithm correctness rely on the mathematics of the application domains, and each domain has its own mathematics.

    In recent years we have applied this method to numerical analysis (algorithms for scientific computing and reasoning about the accuracy of those methods), with machine-checked proofs formally connected to low-level program-correctness proofs.  I will discuss results in the numerical integration of differential equations and in solving linear systems.  Some of these results are joint work with Ariel Kellison and David Bindel (Cornell), Mohit Tekriwal and Jean-Baptiste Jeannin (Michigan). 

Bio: Andrew W. Appel is Eugene Higgins Professor of Computer Science at Princeton University, where he has been on the faculty since 1986. He served as Department Chair from 2009-2015. His research is in software verification, computer security, programming languages and compilers, and technology policy. He received his A.B. summa cum laude in physics from Princeton in 1981, and his PhD in computer science from Carnegie Mellon University in 1985. He is a Fellow of the ACM (Association for Computing Machinery). He has worked on fast N-body algorithms (1980s), functional programming via Standard ML of New Jersey (1990s), Foundational Proof-Carrying Code (2000s), Verified Software Toolchain (2010s), Verified Network Toolchain and Verified Numerical Methods (2020s). His public policy research focuses on voting machines and election systems: technology, security, policy.