Practical Tactics for Verifying C Programs in Coq

Abstract

Proof automation is essential for large scale proof development such as OS kernel verification. An effective approach is to develop tactics and SMT solvers to automatically prove verification conditions. However, for complex systems, it is almost impossible to achieve fully automated verification and human interactions are unavoidable. So the key challenge here is, on the one hand, to reduce manual proofs as much as possible, and on the other hand, to provide user-friendly error messages when the automated verification fails, so that users could adjust specifications or the code accordingly, or to do part of the proofs manually.