Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses

Benchmarks

  1. binary_division
  2. fast_multiplication_2
  3. fast_multiplication_3
  4. fibonacci
  5. Dijkstra_fusc
  6. greatest_common_divisor
  7. hanoi
  8. integer_division
  9. 91-function (rec)
  10. integer_multiplication
  11. lucas
  12. padovan
  13. perrin
  14. remainder
  15. sum_first_integers
  16. digits10
  17. digits10-itmd
  18. digits10-opt
  19. digits10-opt100

Tool