ProB - B2SAT Artifact for FM'2024

<p>This artifact accompanies the paper "B2SAT: A Bare-Metal Reduction of B to SAT" to appear in the proceedings of the FM'2024 conference.&nbsp;The artefact enables one to reproduce the results in the paper.</p> <p>B2SAT is a new SAT backend for the B-Method to enable new applications of formal methods.<br>The new backend interleaves low-level SAT solving with high-level constraint solving.<br>The backend is integrated into ProB, not as a general purpose backend, but<br>as a dedicated backend for solving hard constraint satisfaction and optimisation problems<br>on complex data.&nbsp;<br>A documentation page for B2SAT is available at:<br>&nbsp; <a href="https://prob.hhu.de/w/index.php?title=B2SAT">https://prob.hhu.de/w/index.php?title=B2SAT</a></p> <p>To experiment or reproduce the results download and unpack this artifact (<code>b2sat_artifact.tgz</code>) then you can type the following commands to see help (make help), install ProB inside the folder (make install_prob), run a simple test (make simple) and then re-run the experiments:</p> <p><code>cd benchmarks<br>make help<br>make install_prob<br>make simple<br>make bench<br>make cdclt</code></p> <p>The Makefile of the artifact will download the version 1.13.1-beta1 of ProB for your platform. Note: on macOS you may to have to run make post_install after make install_prob. You also need to have Java 8 or newer installed on your machine.</p> <p>The artifact's Makefile works on macOS and Linux. Even though ProB also works on Windows this artifact is <strong>not</strong> designed for Windows (you will need to adapt the Makefile or by extracting the zip archive manually using Explorer and updating the PATH of your shell manually using `export PATH=$PATH:PROB`; there may also be issues launching the Kodkod backend on Windows).</p> <p>The Linux version of ProB is also available as another artifact:<br>&nbsp; &nbsp; &nbsp; &nbsp; <a href="../records/12166295">ProB Linux 1.13.1.beta1 Zenodo artifact</a> (https://zenodo.org/records/12166295).</p> <p>This version of ProB can be run inside the ifm2022 virtual box machine (<a href="../records/5794839">https://zenodo.org/records/5794839</a>).</p> <p>These are the steps needed to run the benchmarks in the&nbsp;<a href="../records/5794839">iFM2022 virtual machine:</a></p> <p><br><code>sudo apt install curl</code><br><code>mkdir b2sat</code><br><code>cd b2sat</code><br><code>curl -L https://zenodo.org/records/12180216/files/b2sat_artifact.tgz?download=1 -o artifact.tgz</code><br><code>shasum -a 256 artifact.tgz</code><br><code>tar -xvzf artifact.tgz</code><br><code>cd benchmarks</code><br><code>make install_prob</code><br><code>make simple</code><br><code>make bench</code><br><code>make cdclt</code><br><br></p> <p>Note: sometimes on Linux Z3 unfortunately runs out of memory or generates the assertion violation UNEXPECTED CODE WAS REACHED during make bench. You can run&nbsp;<code>make sat</code> to just run B2SAT on the benchmark models. Depending on your Linux system you may also have to set the dynamic library path before running make bench:</p> <p><code>LD_LIBRARY_PATH=PROB/ProB/lib/ make bench</code></p> <p>ProB is based on research and implementation efforts by many people, see&nbsp;<a href="https://prob.hhu.de/w/index.php?title=Team">https://prob.hhu.de/w/index.php?title=Team</a>.</p> <p>To cite ProB you can use this article:&nbsp;<a href="http://dx.doi.org/10.1007/s10009-007-0063-9">http://dx.doi.org/10.1007/s10009-007-0063-9</a>.<br>The original article was published in 2003 at FME: <a href="https://rdcu.be/cKLIv">https://rdcu.be/cKLIv</a>.</p>