Abstract:
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 methods (algorithms for scientific computing) and numerical analysis (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 Appel is Eugene Higgins Professor Computer Science, and served from 2009-2015 as Chair of Princeton's CS department. 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 Ph.D. in computer science from Carnegie Mellon University in 1985. Professor Appel has been editor in chief of ACM Transactions on Programming Languages and Systems and is a fellow of the ACM (Association for Computing Machinery). He has worked on fast N-body algorithms (1980s), Standard ML of New Jersey (1990s), Foundational Proof-Carrying Code (2000s), and the Verified Software Toolchain (2010-present).