Abstract:
In this talk we give an introduction to Mirrorsolve, a Coq library for solving Coq proofs using SMT solvers. Foundational theorem provers such as Isabelle/HOL and Coq are the gold standard for building certified systems, enabling the verification of extremely rich properties while having a minimal trusted code base. Unfortunately, these provers come with a corresponding manual proof burden, as proof engineers must manually construct proofs using low-level steps in the prover’s logic. In this work we combine certified metaprogramming with ideas from automated verification to soundly translate between high-level Coq goals and goals in first-order logic. This translation enables the verification muscle of modern SMT solvers to make use of the natural inductive reasoning available within interactive proof assistants, resulting in full automation for a large variety of common Coq proofs.
In this talk, we first give a gentle introduction to proofs in Coq. Next, we give a brief demo of Mirrorsolve’s automation in practice. Finally we conclude with a gentle discussion of the theory behind the tool, as well as a survey of future directions for the work.
Bio:
John Sarracino is a postdoctoral researcher at Cornell, working with Greg Morrisett. His research interests lie at the intersection of Programming Languages (PL), Security, and Human-Computer Interaction (HCI), and he is interested in developing secure and robust systems using foundational verification, and broadening the impact and adoption of formal methods through proof engineering and language design.
He defended his PhD at UCSD in 2020, working with Nadia Polikarpova and Sorin Lerner in the Programming Systems group. He can be reached at jsarracino -at- cornell.edu.
Galois was pleased to host this tech talk via live-stream for the public. A video of the presentation can be found above.