Download PDFOpen PDF in browserExtending VIAP to Handle Array ProgramsEasyChair Preprint 393, version 212 pages•Date: August 3, 2018AbstractIn 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 SV-COMP 2018 competition, VIAP with array extension came in second in the ReachSafety-Arrays sub-category, behind VeriAbs. Keyphrases: Automatic Program Verification, Mathematical Induction, Nested, Recurrences, SMT, arithmetic, array, first-order logic, multi-dimensional
|