Formally Verifying Imperative Programs
José Pedro Magalhães · 2007
We present a view on the problem of formal verification of imperative programs. Formal verification is usually associated to functional programming languages, but a real-world application will probably be written in imperative main-stream languages. To have the power of formal verification in an imperative language, we present, for demonstrative purposes, an instance of a technique to extend a language with support for logical annotations. We present a short description of LISS (the imperative language chosen to be extended) and Why (the verification condition generator), and after a detailed analysis of the mechanisms used to generate proof-obligations, we conclude, analyzing the global quality of the result.