VIAP

Verifier Integer Assignment Program(VIAP) translates a program to first-order logic with quantifiers on natural numbers following the method proposed recently by Professor Fangzhen Lin . Once translated to a first-order theory, properties of the program can then be proved using induction (because of the quantifiers on natural numbers) and other methods.

• VIAP was second in the ReachSafety-Arrays sub-category of ReachSafety category in SV-COMP 2018
• VIAP was first in the ReachSafety-Arrays sub-category of ReachSafety category in SV-COMP 2019
• VIAP was first in the ReachSafety-Recursive sub-category of ReachSafety category in SV-COMP 2019

• A Formalization of Programs in First-Order Logic with a Discrete Linear Order,Fangzhen Lin,Artificial Intelligence(2016)
• VIAP - automated system for verifying integer assignment programs with loops,Pritom Rajkhowa, Fangzhen Lin, 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing,SYNASC 2017, Timisoara, Romania, September 21-24, 2017
• VIAP-Automated System for Verifying Integer Assignment Programs with Loops(Competition Contribution), Pritom Rajkhowa, Fangzhen Lin, 7th International Competition on Software Verification (2018)(not part of TACAS proceeding)
• Extending VIAP to Handle Array Programs, Pritom Rajkhowa, Fangzhen Lin, 10th Working Conference on Verified Software: Theories, Tools, and Experiments. Sept. 2018
• VIAP 1.1(Competition Contribution), Pritom Rajkhowa, Fangzhen Lin, 25th TACAS at ETAPS 2019: Prague, Czech Republic