https://doi.org/10.6084/m9.figshare.11875428.v1
VAJRA is the implementation that accompanies our paper: "Verifying Array Manipulating Programs with Full-program Induction". Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat. In TACAS 2020.
Vajra accepts a c program annotated with an assertion as input and checks if the assertion holds or not using the full-program induction technique.
VAJRA/bin folder contains the vajra binary compiled on Ubuntu 18.04 LTS as well as the libraries that it depends on. Following the instructions in VAJRA/bin/Readme.txt for installing and using the pre-compiled binary.
Install the following dependencies:
sudo apt-get -y install git g++ cmake libboost-regex-dev libboost-program-options-dev libboost-filesystem-dev libboost-system-dev flex bison
sudo apt-get install clang-6.0 clang-6.0-doc clang-6.0-examples clang-format-6.0 clang-tidy-6.0 clang-tools-6.0 cups-browsed libclang-6.0-dev libclang-common-6.0-dev libclang1-6.0 libllvm6.0 llvm-6.0 llvm-6.0-dev llvm-6.0-runtime python-clang-6.0 clang++-6.0
Some package names may not be exact.
Compilation requires an active internet connection as it fetches the latest Z3 sources.
To compile, navigate to the VAJRA folder and run
make
which will result in the file vajra
in the VAJRA folder.
A C program file annotated with an assertion is to be given as input.
./vajra [file]
Example:
./vajra ../tacas2020-benchmarks/brs1.c
Vajra help:
./vajra --help
Outputs VAJRA_VERIFICATION_SUCCESSFUL for safe programs
Outputs VAJRA_VERIFICATION_FAILED for unsafe programs
Outputs VAJRA_UNKNOWN when the result cannot be determined
Kindly write to [email protected] for any feedback, suggestions, queries and issues.