11:50 am,Lecture Hall 803
The Kernel of Truth: Trust and Verification in Proof Systems
SRI International Menlo Park, CA.
On the one hand, we would like verification tools to feature powerful automation, but on the other hand, we also want to be able to trust the results with a high degree of confidence. The challenge of trust in verification tools has been debated for a long time. One popular way of achieving trust in verification tools is through proof generation. However, proof generation could hamstring both the functionality and the efficiency of the automation that can be built into these tools. We argue that trust need not be achieved at the expense of automation, and outline a lightweight approach called the Kernel of Truth in which the certificates and results from untrusted verifiers can be validated by checkers that have been verified with respect to a trusted proof kernel. We show a few steps toward this goal of building an ecosystem for the certification of claims from automated reasoning tools.