Published June 17, 2024
| Version v1
Software
Open
Integrating Loop Acceleration into Bounded Model Checking
Description
The provided artifact contains the tools that were used for the evaluation of
our paper "Integrating Loop Acceleration into Bounded Model Checking": LoAT, Z3,
Golem, and Eldarica. Moreover, it contains the examples that were used for the
evaluation of our paper: The benchmarks from the category "Linear CHCs, Linear
Integer Arithmetic" from the CHC competition 2023.
Files
artifact.zip
Files
(2.2 GB)
| Name | Size | Download all |
|---|---|---|
|
md5:10eacb786027091778bf76a14d26b4c3
|
2.2 GB | Preview Download |
|
md5:22428108457df7d78aab3fdfbc6ccab3
|
765 Bytes | Download |
|
md5:eb095d6be1efebd7adbac02803b03cf4
|
1.5 kB | Download |
|
md5:94ffc6826c153bd2f0188ce521c35dc5
|
1.1 kB | Download |
|
md5:7702f203b58979ebbc31bfaeb44f219c
|
35.1 kB | Download |
|
md5:5f03ad1486a2e4ce71200ce0f9721557
|
1.1 kB | Download |
Additional details
Related works
- Is supplement to
- Publication: 10.48550/arXiv.2401.09973 (DOI)
Funding
- Deutsche Forschungsgemeinschaft
- Automated Termination and Complexity Analysis of Imperative Programs GI 274/6-2
Software
- Repository URL
- https://github.com/LoAT-developers/LoAT/tree/fm24
- Programming language
- C++