VIAP - Automated System for Verifying Integer Assignment Programs with Loops

摘要

This paper describes an automated system, VIAP, for proving the correctness of procedural programs with integer assignments and loops. VIAP does not require loop-invariants to verify the correctness of programs. It also includes functionalities resulting from the extension of existing work about program translation into FOL by solving recurrences generated during translation. This system is also able to prove partial correctness of programs, given precondition(s) and postcondition(s), without using loop invariants. We validate these claims by showing that VIAP can successfully prove the benchmark programs used by invariant-generating tools in literature for their validation, without the requirement of the generation of these loop-invariants. The system is fully automatic and points to a new way of proving properties of programs.