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, but
as a dedicated backend for solving hard constraint satisfaction and optimisation problems
on 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 benchmarks
make help
make install_prob
make simple
make bench
make 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. You also need to have Java 8 or newer installed on your machine.

The artifact's Makefile works on macOS and Linux. Even though ProB also works on Windows this artifact is not 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).

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 curl
mkdir b2sat
cd b2sat
curl -L https://zenodo.org/records/12180216/files/b2sat_artifact.tgz?download=1 -o artifact.tgz
shasum -a 256 artifact.tgz
tar -xvzf artifact.tgz
cd benchmarks
make install_prob
make simple
make bench
make cdclt

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 make sat 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:

LD_LIBRARY_PATH=PROB/ProB/lib/ make bench

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.