Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses
Benchmarks
- binary_division
- fast_multiplication_2
- fast_multiplication_3
- fibonacci
- Dijkstra_fusc
- greatest_common_divisor
- hanoi
- integer_division
- 91-function (rec)
- integer_multiplication
- lucas
- padovan
- perrin
- remainder
- sum_first_integers
- digits10
- digits10-itmd
- digits10-opt
- digits10-opt100
Tool