VIAP : an automated system for verifying integer assignment programs with loops

Abstract

Automatic program verification has been a major research area since its beginning. Despite significant progress in automatic program verification, proving the correctness of programs with loops and arrays is still considered as a complex problem. In this thesis, we describe a fully automated verifier for programs with loops based on new approach proposed by Lin [98]. We call our system VIAP, short for a Verifier for Integer Assignment Programs. Given a program and a requirement to verify, it first translates the given program into a set of first-order axioms independent of the requirement. The requirement is then verified as a query of the translated axioms. What distinguishes VIAP is its handling of loops. The iterations are systematically encoded as inductive definitions, and the termination is axiomatised by constraints on specially introduced constants. The efficiency of VIAP comes from many simplifying techniques, including a dedicated recurrence solver to compute the closed-form solutions of inductive definitions whenever possible. As a result, VIAP is able to automatically prove non-trivial properties of many benchmark programs that previously require either manually encoded loop invariants or powerful loop invariant generators. VIAP was entered in the SV-COMP 2019 competition and scored first in the ReachSafety-Arrays and ReachSafety-Recursive sub-categories of the ReachSafety category.

Date of Award	2019
Original language	English
Awarding Institution	The Hong Kong University of Science and Technology