This is the empirical evaluation of the implementation of our techniques from the paper Accelerated Bounded Model Checking in our tool LoAT.
Getting LoAT
We provide a pre-compiled binary of LoAT (Linux, 64 bit). Moreover, you can find the source code of LoAT at GitHub. An artifact containing LoAT which allows to replicate our experiments is available at Zenodo.
We refer to the general LoAT website for further information.
Evaluation
Examples
We used the examples from the category LIA-Lin (linear CHCs with linear integer arithmetic) from the CHC competition 2023. They can be found here.
Tools
In our evaluation, we considered the following tools and configurations:- LoAT 0.7.0
- Accelerated Bounded Model Checking with blocking clauses (LoAT ABMC_b)
- loat-static --mode reachability --format horn --engine abmc $INPUT
- Accelerated Bounded Model Checking without blocking clauses (LoAT ABMC)
- loat-static --mode reachability --format horn --engine abmc --abmc::blocking_clauses false $INPUT
- Bounded Model Checking (LoAT BMC)
- loat-static --mode reachability --format horn --engine bmc $INPUT
- Acceleration Driven Clause Learning (LoAT ADCL)
- loat-static --mode reachability --format horn --engine adcl $INPUT
- Z3 4.13.0
- the Spacer algorithm (Spacer)
- z3 fp.engine=spacer $INPUT
- Bounded Model Checking (Z3 BMC)
- z3 fp.engine=bmc $INPUT
- Golem 0.5.0
- Transition Power Abstraction (Golem TPA)
- golem -l QF_LIA -e split-tpa $INPUT
- Bounded Model Checking (Golem BMC)
- golem -l QF_LIA -e bmc $INPUT
- Eldarica 2.1.0
- CEGAR with acceleration as preprocessing
- eld -splitClauses:1 -abstract:off -stac $INPUT
- Symbolic Execution
- eld -splitClauses:1 -sym $INPUT