Skip to main content

Perspectives on formal verification (invited talk)

Harvey M. Friedman

Publisher page dblp BibTeX

Abstract

I will discuss the importance, uses, and future directions of formal verification from the point of view of a mathematical foundationalist. These include issues of certainty, proof structure, and (finitary) completeness and decidability.

DOI 10.1145/2854065.2858808

Related papers

The sel4 verification: the art and craft of proof and the reality of commercial support (invited talk) CPP 2022
Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk) CPP 2019
Practical Verification for the Working Programmer with CodeContracts and Abstract Interpretation - (Invited Talk) VMCAI 2011
Combining functional programming and hardware verification (abstract of invited talk) ICFP 2000
Formal Analysis of Message Passing - (Invited Talk) VMCAI 2011
Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper) CPP 2018
Coq's vibrant ecosystem for verification engineering (invited talk) CPP 2022
Prospects for Computer Formalization of Infinite-Dimensional Category Theory (Invited Talk) CPP 2025