Certified Reasoning for Automated Verification

Abstract :

Formal methods help improve the quality and reliability of software by providing proof of
correctness. However, ensuring the correctness of verification tools that apply these formal
methods, is itself a much harder problem. A typical way to justify the correctness is to provide
soundness proofs based on semantic models. For program verifiers these soundness proofs are
quite large and complex. In this thesis, we introduce certified reasoning to provide machine
checked proofs of various components of an automated verification system. We develop new
certified decision procedures (Omega++) and certified proofs (for compatible sharing)
and integrate with an existing automated verification system (HIP/SLEEK). We show that
certified reasoning improves the correctness and expressivity of automated verification
without sacrificing on performance.