Welcome, PERR 2019 participants!

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.

• Slides

  Download the slides of the presentation.

• Try the RMT equivalence checker online

  Go to RMT online.

• Installation and Compilation of RMT

  Requirements:

  • CMake
  • A modern C++ compiler such as GCC or Clang

  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
  cd z3
  mkdir buildz3
  cd buildz3
  cmake ..
  make

  Once Z3 compiled, please download RMT using git:

  git clone https://github.com/ciobaca/rmt
  cd rmt
  mkdir buildrmt
  cd buildrmt
  cmake .. -DZ3_DIR=~/pathtoz3/buildz3
  make

  Running RMT to Prove Equivalence

  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

• Trouble or questions?

  Please fire an email to stefan.ciobaca@gmail.com.