Download PDFOpen PDF in browserCurrent version

Extending VIAP to Handle Array Programs

EasyChair Preprint no. 393, version 1

Versions: 12history
12 pagesDate: August 2, 2018


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: arithmetic, array, Automatic Program Verification, first-order logic, Mathematical Induction, multi-dimensional, Nested, Recurrences, SMT

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Pritom Rajkhowa and Fangzhen Lin},
  title = {Extending VIAP to Handle Array Programs},
  howpublished = {EasyChair Preprint no. 393},
  doi = {10.29007/pjbm},
  year = {EasyChair, 2018}}
Download PDFOpen PDF in browserCurrent version