VIAP-Automated System for Verifying Integer Assignment Programs with Loops

PhD Thesis Proposal Defence


Title: "VIAP-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. The main difficulty in proving the correctness of 
programs with loops and array in traditional approaches is that it is not 
always possible to find the number iterations statically. In such cases, they 
tried to derive a logical property called the loop invariant which describes 
the properties of loops in each iteration. It provides a solution to this 
problem so that reasoning about loop becomes independent of the number of 
iterations. Although the automatic generation of loop invariants itself is 
considered as a long-standing complex problem. In the case of programs that use 
non-linear arithmetic, unbounded data structures like array, complex control 
flow (such as nested loops), it is difficult to automatically find suitable 
candidate invariants. That's why the automatic generation of suitable loop 
invariants is one of the major practical obstacles to full automation of 
program verification.

To address that challenge, Lin proposed a method for translating a 
non-concurrent program to a first-order theory with quantifiers over natural 
numbers. This approach does not rely on loop invariants. Once translated to a 
first-order theory, properties about the program can then be proved using 
induction (because of the quantifiers on natural numbers) and other methods. 
This approach has been implemented a fully automated system VIAP, short for a 
Verifier for Integer Assignment Programs, for proving the correctness of 
procedural programs. We improved the approach by integrating recurrence 
solver(RS) which try to compute the closed-form solutions of inductive 
definitions in Lin's translation. VIAP use SMT solver Z3 as the basic theorem 
prover. RS uses SymPy's rsolve() function as a base solver and extends it to 
handle conditional recurrences. It also includes a solution for a simple case 
of mutual recurrences. It successfully proves benchmark programs such as those 
for computing integer square roots, integer product, integer power, factorial 
and the sums of series of integers. The system is fully automatic and points to 
a new way of proving properties of programs.

In the most recent SV-COMP 2019 competition, VIAP came first in the 
ReachSafety-Arrays and ReachSafety-Recursive sub-category. In SV-COMP 2018 
competition, VIAP also came in second in the ReachSafety-Arrays sub-category, 
behind VeriAbs.

Program equivalence checking has significant practical applications such as 
compiler optimization validation, information flow analysis, and regression 
verification. Program equivalence checking also presents the same challenges as 
program verification. We have extended the approach designed fully automated 
system called Eq-VIAP primarily for checking the equivalence of programs.


Date:			Wednesday, 6 March 2019

Time:                  	10:00am - 12:00noon

Venue:                  Room 2405
                         (lifts 17/18)

Committee Members:	Prof. Fangzhen Lin (Supervisor)
 			Prof. Shing-Chi Cheung (Chairperson)
 			Prof. Cunsheng Ding
 			Dr. Ke Yi


**** ALL are Welcome ****