THESIS
2019
xii, 129 pages : illustrations (one color) ; 30 cm
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...[
Read more ]
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.
Post a Comment