Abstract: What do we need in a practical program logic and tool for verifying C programs? It must support pointer data structures with sharing and mutation: separation logic is useful. It should facilitate the use of function pointers in such usage patterns as “objects” or “closures”: it should be higher-order. It should support data abstraction, especially in connection with objects and closures; that is, quantification over representation predicates.
Each program is verified in its own application domain, so the program logic should have strong facilities and libraries for reasoning in the mathematics of many application domains. So the program logic be embedded in a general-purpose logic and proof assistant such as Coq.
Verifiable C is a higher-order concurrent separation logic for C, embedded in Coq, as part of the Verified Software Toolchain. It is proved sound with a machine-checked proof in Coq. It assists users in interactively building correctness proofs for their C programs. In this talk I will explain the requirements, design, implementation, and practical use of the Verified Software Toolchain.
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 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 (2010s).