This is a tool for program verification that uses the theories of Constraint Horn Clauses and an algorithm based on the weakest liberal precondition algorithm seen in the paper Horn Clause Solvers for Program Verification by Nikolaj Bjørner et al..
Install Java
sudo apt-get update
sudo apt-get install default-jdkInstall Python3
sudo apt-get install python3 Install Scala 2.11.12
sudo apt-get install scalaUse the package manager pip to install Z3.
sudo apt install python3-pip
pip install z3-solverInside the src folder where the tool.scala file lies run:
scala -nc tool.scala ../FILEPATH/inputFile.txt [-bv BitVectorSize]The optional parameter -bv determines if bitvector arithmetic is to be used instead of integer arithmetic and the BitVectorSize determines its size. The BitVectorSize argument is mandatory if the -bv flag is used.
When writing programs note that there is no no operator precedence. In this case this can be achieved by using parentheses in the right way. See the following examples for more explanation.
x := 1 + 2 / 3 + 4 => Wrong Evaluation
x := 1 + 2 / (3 + 4) => Wrong Evaluation
x := (1 + 2) / (3 + 4) => Right Evaluation
x := (1 + 2) / (3 + 4) / (4 + 5) => Wrong Evaluation
x := ((1 + 2) / (3 + 4)) / (4 + 5) => Right Evaluation