This tool is a product of our works reported below:

• An Equivalence Checking Framework for Array-Intensive Programs, ATVA 2017
• Translation Validation of Loop and Arithmetic Transformations in the Presence of Recurrences, LCTES 2016
• Verification of Loop and Arithmetic Transformations of Array-Intensive Behaviors, TCAD 2013
• Equivalence Checking of Array-Intensive Programs, ISVLSI 2011

Pre-requisites:

• gcc 4.7.2
• flex 2.5.35
• bison 2.5
• barvinok-0.36 (Integer Set Library)

Please execute the following commands to install and run ADDG.

/***********************************************************************/

make <-- This will install ADDG Equivalence Checker.

cd bin

./eqChkAddg file1.c file2.c <-- To run ADDG Equivalence Checker.

/***********************************************************************/

NB: You are required to modify the path to ISL as defined by the variable "PATH_ISL" on line 8 of Makefile.

Some benchmarks are provided in the folder "Benchmarks".

Please note the following restrictions on the input C files:

• Should have a single function.
• Should not have bitwise operators, pointers, user-defined data structures like struct, enum, etc.
• Should not have while, do..while loops, i.e., only "for" loops are allowed.

If you use this tool, then please cite the following work:
@inproceedings{BanerjeeMS17,
author = {Kunal Banerjee and Chittaranjan Mandal and Dipankar Sarkar},
title = {An Equivalence Checking Framework for Array-Intensive Programs},
booktitle = {Automated Technology for Verification and Analysis - 15th International Symposium, {ATVA} 2017, Pune, India, October 3-6, 2017, Proceedings},
pages = {84--90},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-68167-2_6},
doi = {10.1007/978-3-319-68167-2_6},
}

For more information (and on discovery of bugs), please contact: [email protected]