Extending VIAP to Handle Array Programs

EasyChair Preprint 393, version 1

Abstract

In this paper, we extend our previously described fully automated program verification system called VIAP primarily for verifying the safety properties of programs with integer assignments to programs with arrays. VIAP is based on a recent
translation of programs to first-order logic proposed by Lin \cite{Lin20161}
and directly calls the SMT solver Z3. It relies more on reasoning with
recurrences instead of loop invariants. In this paper, we extend it to programs with arrays. Our extension is not restricted to single dimensional arrays but general and works for multidimensional and nested arrays as well. In the most recent 
\textit{SV-COMP} 2018 competition, VIAP with array extension came in second
in the ReachSafety-Arrays sub-category, behind \textit{VeriAbs}.

Keyphrases: Automatic Program Verification, Mathematical Induction, Nested, Recurrences, SMT, arithmetic, array, first-order logic, multi-dimensional

@booklet{EasyChair:393,
  author    = {Pritom Rajkhowa and Fangzhen Lin},
  title     = {Extending VIAP to Handle Array Programs},
  doi       = {10.29007/pjbm},
  howpublished = {EasyChair Preprint 393},
  year      = {EasyChair, 2018}}