Artifact for the TACAS 2025 paper "Refuting Equivalence in Probabilistic Programs with Conditioning"

<p dir="ltr">This repository contains the artifact of the paper titled "Refuting Equivalence in Probabilistic Programs with Conditioning" accepted at TACAS 2025.<br><br>The tool takes two probabilistic transition systems with specified initial configurations as input and based on user preferences either (i) tries to prove whether the two programs generate equivalent output distributions, or (ii) tries to find a lowerbound on Kantorovich distance between the output distributions of the input programs.<br><br>In order to run the baseline, Mathematica (`math` command in terminal) must be installed.<br><br>Additionally, the repository contains the files for Gurobi Optimizer v10.0.3.</p>