The Last Mile in Trustworthy Automated Reasoning
Abstract:
State-of-the-art automated reasoning tools are complex and highly-optimized pieces of software. This complexity can lead to an increased risk of soundness-critical bugs, which may affect the trustworthiness of automatically generated results. To remedy this state of affairs, many tools now generate proof logs (or proof certificates), which can be independently checked for correctness.
This talk is about the "last mile" in highly trustworthy automated reasoning---the development of efficient, formally verified proof checkers that are capable of soundly scrutinizing proof logs for various theories. I will briefly explain how automated reasoning tools can be augmented to generate proof logs, using SAT solvers as an example. Then, I will survey theories, proof systems, and proof checkers that have been formalized in proof assistants, including my work with various collaborators on verifying proof checkers using HOL4 and CakeML.
Biodata:
Yong Kiam Tan is a research scientist at the Institute for Infocomm Research (I2R), Singapore. He completed his PhD in Computer Science (Pure and Applied Logic) at Carnegie Mellon University, advised by Prof. Andre Platzer. He is interested in formal verification in various areas of computer science, including compilers, hybrid systems, and security.