This is the empirical evaluation of the implementation of our techniques from the paper Infinite State Model Checking by Learning Transitive Relations 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.

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 competitions 2023 and 2024, excluding duplicates. They can be found here (2023) and here (2024).

Tools

In our evaluation, we considered the following tools and configurations:

• LoAT 0.9.0
• Transitive Relation Learning (LoAT TRL)
• loat-static --mode safety --format horn --engine trl $INPUT
• Accelerated Bounded Model Checking (LoAT ABMC)
• loat-static --mode safety --format horn --engine abmc $INPUT
• k-Induction (LoAT KIND)
• loat-static --mode safety --format horn --engine kind $INPUT
• Z3 4.13.3
• Spacer with Global Guidance (Z3 GSpacer)
• z3 fp.engine=spacer fp.spacer.global=true $INPUT
• Spacer (Z3 Spacer)
• z3 fp.engine=spacer $INPUT
• Bounded Model Checking (Z3 BMC)
• z3 fp.engine=bmc $INPUT
• Golem 0.6.2
• Spacer (Golem Spacer)
• golem -l QF_LIA -e spacer $INPUT
• Property Directed k-Induction (Golem PDKIND)
• golem -l QF_LIA -e pdkind $INPUT
• Interpolation Based Model Checking (Golem IMC)
• golem -l QF_LIA -e imc $INPUT
• Transition Power Abstraction (Golem TPA)
• golem -l QF_LIA -e split-tpa $INPUT
• Lazy Abstraction with Interpolants (Golem LAWI)
• golem -l QF_LIA -e lawi $INPUT
• Predicate Abstraction (Golem PA)
• golem -l QF_LIA -e pa $INPUT
• Bounded Model Checking (Golem BMC)
• golem -l QF_LIA -e bmc $INPUT
• Eldarica 2.1.0
• eld $INPUT

Results

Here you can find a table with the detailed results of our benchmarks.

Example from the Paper

Here you can find the leading exmaple from our paper.