ProB - B2SAT Artifact for FM'2024

This artifact accompanies the paper "B2SAT: A Bare-Metal Reduction of B to SAT" to appear in the proceedings of the FM'2024 conference. The artefact enables one to reproduce the results in the paper. B2SAT is a new SAT backend for the B-Method to enable new applications of formal methods.The new backend interleaves low-level SAT solving with high-level constraint solving.The backend is integrated into ProB, not as a general purpose backend, butas a dedicated backend for solving hard constraint satisfaction and optimisation problemson complex data. A documentation page for B2SAT is available at: https://prob.hhu.de/w/index.php?title=B2SAT To experiment or reproduce the results download and unpack this artifact (b2sat_artifact.tgz) 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: cd benchmarksmake helpmake install_probmake simplemake benchmake cdclt 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. The Linux version of ProB is also available as another artifact: ProB Linux 1.13.1.beta1 Zenodo artifact (https://zenodo.org/records/12166295). This version of ProB can be run inside the ifm2022 virtual box machine (https://zenodo.org/records/5794839). These are the steps needed to run the benchmarks in the iFM2022 virtual machine: sudo apt install curlmkdir b2satcd b2satcurl -L https://zenodo.org/records/12166663/files/b2sat_artifact.tgz?download=1 -o artifact.tgzshasum -a 256 artifact.tgztar -xvzf artifact.tgzcd benchmarksmake install_probmake simplemake benchmake cdclt ProB is based on research and implementation efforts by many people, see https://prob.hhu.de/w/index.php?title=Team. To cite ProB you can use this article: http://dx.doi.org/10.1007/s10009-007-0063-9.The original article was published in 2003 at FME: https://rdcu.be/cKLIv.