VIAP - An Automated System for Verifying Integer Assignment Programs with Loops

The Hong Kong University of Science and Technology
Department of Computer Science and Engineering


PhD Thesis Defence


Title: "VIAP - An Automated System for Verifying Integer Assignment Programs 
with Loops"

By

Mr. Pritom RAJKHOWA


Abstract


The 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 new approach proposed by 
Lin. 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 to a set of first-order axioms independent of the 
requirement. The requirement is then verified as a query to 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 some non-trivial properties of many benchmark programs 
that require either manually encoded loop invariants or powerful loop 
invariant generators. VIAP was entered at the SV-COMP 2019 competition and 
scored first in the ReachSafety-Arrays and ReachSafety-Recursive 
sub-categories of the ReachSafety category.


Date:			Monday, 19 August 2019

Time:			9:00am - 11:00am

Venue:			Room 3494
 			Lifts 25/26

Chairman:		Prof. Patrick Yue (ECE)

Committee Members:	Prof. Fangzhen Lin (Supervisor)
 			Prof. Cunsheng Ding
 			Prof. Ke Yi
 			Prof. Wai-Ho Mow (ECE)
 			Prof. Yanhong Liu (Stony Brook University)


**** ALL are Welcome ****