This web page contains additional information regarding our PERR 2019 submission: Ștefan Ciobâcă, Dorel Lucanu and Sebastian Buruiană: Semantics-Based Proofs of Equivalence for Functions with Accumulators.
Go to RMT online.
Please first compile Z3 from here (follow the readme in order to complete the installation). Check that the installation completed successfully by running z3 from the command line. You should obtain a message similar to:
git clone https://github.com/Z3Prover/z3.git
Once Z3 compiled, please download RMT using git:
git clone https://github.com/ciobaca/rmt
cmake .. -DZ3_DIR=~/pathtoz3/buildz3
The equivalence examples are in the folder examples/perr-2019. Run RMT on the first example:
buildrmt/rmt -v 0 examples/perr-2019/accumulator-vs-nonacc-simplified-partial.rmt
Please fire an email to email@example.com.