Automatic Coq Proofs Generation from Static Analyzers by Lightweight Instrumentation

This paper deals with program verification and more precisely with the question of how to provide verifiable evidence that a program verifies certain semantics properties. Program processing tools such as compiler or static analyzers are complex pieces of software which may contain errors. The idea of using analyzers as guessing algorithms and proving the discovered properties by independent means has been proposed a decade ago. However, automatically generating the proofs without user interaction is still a major challenge. We present a methodology of instrumentation of existing static analyzers based on abstract interpretation to make them produce certificates of their results. We apply our methodology on an existing static analyzer that discovers invariants of array-processing programs which can be expressed in first-order logic. Certificates are provided as COQ proofs based on Floyd-Hoare’s method for proving program invariants.