This page contains useful information regarding the integration of the C bounded model chcker CBMC with our SAT solver ParaFROST.

ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NIVIDA CUDA-enabled GPUs in applying modern simplification tecnhiques in parallel. New compact data structure and memory-aware Variable-Clause Eliminations (VCE) are designed specifically for BMC problems in the new version of our tool. Furthermore, the decision making heuristics are further improved.

The GPU-accelerated version of CBMC with ParaFROST has a complete artifact we created to experimentally evaluate the effectiveness of accelerating Boumded Model Checking (BMC) using GPUs on verifying AWS C99 package. The artifact can be downloaded here. Follow the instructions in README to run and evaluate the artifact.

Furthermore, CBMC is patched to read a configuration file before is instantiated. This file contains all options supported by ParaFROST in the format <option>=<value>. The configurable interface allows the user to explore all ParaFROST capabilities while running the verifier. To install and run CBMC with ParaFROST, check our Github repository.