VIAP 1.1
Abstract
VIAP (Verifier for Integer Assignment Programs) is an automated system for verifying safety properties of procedural programs with integer assignments and loops. It is based on a translation from of a program to a set of firstorder axioms with quantification over natural numbers, and currently makes use of SymPy as the algebraic simplifier and the SMT solver Z3 as the theorem prover. Our first version of the system competed at SVCOMP 2018. This paper describes VIAP 1.1, a new version that makes use of our newly developed recurrence solver. As a result, VIAP 1.1. is able to verify many programs that were out of reach for the older version VIAP 1.0.
Keywords
Automatic program verification Firstorder logic Mathematical induction Recurrences SMT Arithmetic1 Introduction
VIAP (Verifier for Integer Assignment Programs) is an automated system for verifying safety properties of procedural programs with integer assignments and loops. It translates a given program to a set of firstorder axioms with natural number quantification using an algorithm proposed by Lin [1]. An earlier version of VIAP competed at SVCOMP 2018, and is described in [2, 3]. A key feature of Lin’s translation is that loops are translated to a set of recurrence relations. Then, VIAP simplifies those axioms by using a Python library for symbolic computation systems, SymPy [4], to compute the closedform solutions of recurrence relations. SymPy is equipped with function rsolve() to compute closedform solution of recurrence relation. The translation of the loop body generates recurrence relations which are either simple nonconditional, conditional or mutual in nature. But rsolve() can find the closed form solution only for certain class of simple nonconditional recurrence relations. This motivated us to design a recurrence solver (RS) that goes beyond what the rsolve() function can do in SymPy, and integrate it with our system. The new system, VIAP 1.1, is the one that will compete at this year’s SVCOMP. VIAP 1.1 continues to use SymPy for simplifying algebraic expressions, and the SMT solver Z3 [5] as the underlying theorem prover without ever explicitly generating loop invariants. Because of the new recurrence solver, VIAP 1.1 can solve many more benchmarks that were previously out of the reach of VIAP 1.0.
2 VIAP Architecture

FrontEnd: The system accepts a program written in C (C99 language) as input and translates it to first order axioms. The recurrence solver solves the recurrence relations generated during the translation if closedform solutions are available.

BackEnd: The system takes the set of translated firstorder axioms and translates all the axioms to equations compatible with Z3 (Version 4.5) by preprocessing them using SymPy (Version 1.1.1). Then the proof engine applies different strategies and tries to prove postconditions in Z3 [2].
Recurrence Solver (RS). The main objective of this module is to find closedform solutions of recurrence relations generated from the translation of the loop body. Our recurrence solver (RS)^{2} takes a set of recurrence relation(s) and other constraints, returns a set of closedform solutions it found for some of the recurrences and the remaining recurrences relations and constraints simplified using the computed closedform solutions. It uses SymPy [4] (V 1.1.1) as the base solver. The RS classifies input recurrence relation(s) into three major categories (1. nonconditional 2. mutual and 3. conditional recurrences relation) and applies the following corresponding subsolver and tries to find closed form solution(s).
 The NonConditional Recurrence Solver (NCRS): RS applies this sub solver to the nonconditional recurrence relation(s) of the form of eitherwhere f(x, y) is a polynomial function of x and y$$\begin{aligned}&X(n+1)=f(X(n),n), \end{aligned}$$orwhere f(n) is a polynomial function in n, \(A_i\)’s are constants, and \(F_i\)’s are function symbols.$$\begin{aligned}&X(n+1) = X(n)+f(n)+A_1F_1(n)+\cdots +A_kF_k(n), \end{aligned}$$
 The Mutual Recurrence Solver (MRS): RS applies this sub solver to a set \(\varvec{\sigma }\) of the mutual recurrence relations where each \(\sigma \in \varvec{\sigma }\) is the form ofwhere A and \(C_i\) are constants.$$\begin{aligned}&X_i(n+1) = A*(X_1(n)+\ldots +X_h(n)) + C_i, \qquad \text {for }1\le i\le h, \end{aligned}$$
 The Conditional Recurrence Solver (CRS): RS applies this sub solver to conditional recurrence relation(s) of the formwhere \(\theta _1,\theta _2,\ldots ,\theta _{h}\) are Boolean expressions, and \(f_1(x,y),f_2(x,y),\ldots ,\) \(f_{h+1}(x,y)\) are polynomial functions of x and y.$$\begin{aligned} X(n+1)= & {} ite(\theta _1,f_1(X(n),n),ite(\theta _2,f_2(X(n),n)\ldots ,f_{h+1}(X(n),n))), \end{aligned}$$
Proof Strategies: As the semantics of P are precisely encoded as \(\varPi _P^{\varvec{X}}\), the goal is to prove that Open image in new window , where \(\alpha \) is a set of assumption(s) and \(\beta \) is the set of assertion(s) to prove. We work in a refutationbased proof schema, i.e., in order to prove that a formula is valid in a background theory T, we show that \(\alpha \wedge \varPi _P^{\varvec{X}} \wedge \lnot \beta \) is Tunsatisfiable. In VIAP, we implemented two different strategies whose details can be found in our previous work [2].
3 Strength and Weaknesses
VIAP supports user assertions, including reachability of labels in the Ccode. In SVCOMP 2019, these checks are only enabled for ReachSafetyArrays, ReachSafetyLoops and ReachSafetyRecursive subcategories of ReachSafety category. VIAP translates a program to a set of axioms and then uses offtheshelf systems like SymPy and Z3 to prove properties about the program. The advantage (strength) of this approach comes with a clean separation between the translation (semantics) and the use of the translation in proving the properties (computation). The translation part is stable. But as more efficient provers become available, the capabilities of the system improve. This is seen in our newer version of VIAP that we entered in this year’s competition: by having a more powerful system for computing closedform solutions of recurrences, the new system becomes more efficient and can prove many properties that our previous system were not able to. However, VIAP provides little or no support for translation and reasoning about dynamic linked data structures or programs with floating points. We are working in the direction to strengthen our frontand backhand to handle all types of the program so that we can participate in all the subcategories of ReachSafety in the future edition of SVCOMP. The SVCOMP’19 results show that VIAP can effectively verify a number C programs from those categories. VIAP came in first in the ReachSafetyArrays and ReachSafetyRecursive subcategory. The major disadvantage of the method which translates loop body to the recurrence relation is that if they failed to find closed form solution, then they unable to find suitable invariant as a result they failed to complete the proof. When VIAP fails to come up with a closedform solution, it falls back to simple induction using Z3. There is clearly a need of better way to do induction and we are working on it. In terms of closedform solution, in general it is undecidable whether a recurrence has a closedform solution or not.
4 Tool Setup and Configuration
SPEC is the property file, and INPUT is a C file. The output of VIAP is “VIAP_OUTPUT_True” when the program is safe. When a counterexample is found, it outputs “VIAP_OUTPUT_False” and a file named errorWitness.graphml that contains the witness of errorpath is generated in the VIAP root folder. If VIAP is unable find any result it outputs “UNKNOWN”.
5 Software Project and Contributors
VIAP is an opensource project, mainly developed by Pritom Rajkhowa and Professor Fangzhen Lin of the Hong Kong University of Science and Technology. We are grateful to the developers of Z3 and SymPy for making their systems available for open use.
Footnotes
Notes
Acknowledgments
We are very thankful to the anonymous reviewers for their helpful comments on an earlier version of this paper.
References
 1.Lin, F.: A formalization of programs in firstorder logic with a discrete linear order. Artif. Intell. 235, 1–25 (2016)MathSciNetCrossRefGoogle Scholar
 2.Rajkhowa, P., Lin, F.: VIAP  automated system for verifying integer assignment programs with loops. In: Jebelean, T., Negru, V., Petcu, D., Zaharie, D., Ida, T., Watt, S.M. (eds.) 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2017, Timisoara, Romania, 21–24 September 2017, pp. 137–144. IEEE Computer Society (2017)Google Scholar
 3.Rajkhowa, P., Lin, F.: Extending VIAP to handle array programs. In: Piskac, R., Rümmer, P. (eds.) VSTTE 2018. LNCS, vol. 11294, pp. 38–49. Springer, Cham (2018). https://doi.org/10.1007/9783030035921_3CrossRefGoogle Scholar
 4.SymPy Development Team: SymPy: python library for symbolic mathematics (2016)Google Scholar
 5.de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540788003_24CrossRefGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.