The proofs generated by KoAT can be downloaded here.
| Example | Result | Runtime |
|---|---|---|
| prob_cfr/cfr01.koat | O(1) | 1.16 s |
| prob_cfr/cfr02.koat | O(n) | 1.62 s |
| prob_cfr/cfr03.koat | O(n) | 2.63 s |
| prob_cfr/cfr04.koat | O(n) | 4.50 s |
| prob_cfr/cfr05.koat | O(n) | 3.42 s |
| prob_cfr/cfr06.koat | O(n) | 3.87 s |
| prob_cfr/cfr07.koat | O(n) | 2.03 s |
| prob_cfr/cfr08.koat | O(n) | 6.46 s |
| prob_cfr/cfr09.koat | O(n) | 1.51 s |
| prob_cfr/cfr10.koat | O(n) | 2.78 s |
| prob_cfr/cfr11.koat | O(n) | 1.53 s |
| prob_cfr/cfr12.koat | O(n) | 2.78 s |
| prob_cfr/cfr13.koat | O(n) | 0.93 s |
| prob_cfr/cfr14.koat | O(1) | 3.33 s |
| prob_cfr/cfr15.koat | Maybe | 2.90 s |
| Absynth-Suite/2drwalk.koat | O(n) | 38.94 s |
| Absynth-Suite/C4B_t09.koat | O(n) | 0.72 s |
| Absynth-Suite/C4B_t13.koat | O(n) | 0.70 s |
| Absynth-Suite/C4B_t15.koat | O(n) | 0.67 s |
| Absynth-Suite/C4B_t19.koat | O(n) | 0.78 s |
| Absynth-Suite/C4B_t30.koat | O(n) | 0.80 s |
| Absynth-Suite/C4B_t61.koat | O(n) | 0.59 s |
| Absynth-Suite/bayesian.koat | O(n) | 4.61 s |
| Absynth-Suite/ber.koat | O(n) | 0.48 s |
| Absynth-Suite/bin.koat | O(n) | 0.58 s |
| Absynth-Suite/complex.koat | O(n²) | 6.21 s |
| Absynth-Suite/condand.koat | O(n) | 0.43 s |
| Absynth-Suite/cooling.koat | O(n) | 0.97 s |
| Absynth-Suite/coupon.koat | O(1) | 1.41 s |
| Absynth-Suite/cowboy_duel.koat | O(1) | 0.61 s |
| Absynth-Suite/cowboy_duel_3way.koat | O(1) | 2.18 s |
| Absynth-Suite/fcall.koat | O(n) | 2.06 s |
| Absynth-Suite/filling.koat | O(n) | 2.37 s |
| Absynth-Suite/geo.koat | O(1) | 0.54 s |
| Absynth-Suite/hyper.koat | O(n) | 0.69 s |
| Absynth-Suite/linear01.koat | O(n) | 0.40 s |
| Absynth-Suite/miner.koat | O(n) | 2.11 s |
| Absynth-Suite/multirace.koat | Maybe | 5.51 s |
| Absynth-Suite/no_loop.koat | O(1) | 0.30 s |
| Absynth-Suite/pol04.koat | Maybe | 9.31 s |
| Absynth-Suite/pol05.koat | Maybe | 3.65 s |
| Absynth-Suite/pol06.koat | O(1) | 3.72 s |
| Absynth-Suite/pol07.koat | O(n²) | 2.90 s |
| Absynth-Suite/prdwalk.koat | O(n) | 0.84 s |
| Absynth-Suite/prnes.koat | O(n) | 1.84 s |
| Absynth-Suite/prseq.koat | O(n) | 0.85 s |
| Absynth-Suite/prseq_bin.koat | O(n) | 1.05 s |
| Absynth-Suite/prspeed.koat | O(n) | 4.95 s |
| Absynth-Suite/race.koat | O(n) | 0.81 s |
| Absynth-Suite/rdbub.koat | O(n²) | 4.17 s |
| Absynth-Suite/rdseql.koat | O(n) | 0.66 s |
| Absynth-Suite/rdspeed.koat | O(n) | 1.12 s |
| Absynth-Suite/rdwalk.koat | O(n) | 0.88 s |
| Absynth-Suite/rfind_lv.koat | O(1) | 0.68 s |
| Absynth-Suite/rfind_mc.koat | O(n) | 0.77 s |
| Absynth-Suite/robot.koat | O(n) | 3.82 s |
| Absynth-Suite/roulette.koat | O(n) | 3.11 s |
| Absynth-Suite/sampling.koat | O(n) | 2.20 s |
| Absynth-Suite/simple_recursive.koat | O(n) | 0.78 s |
| Absynth-Suite/sprdwalk.koat | O(n) | 0.92 s |
| Absynth-Suite/trader.koat | Maybe | 16.46 s |
| KoAT-Suite/C4B_t132.koat | O(n) | 0.71 s |
| KoAT-Suite/alain.c.koat | O(n³) | 12.28 s |
| KoAT-Suite/complex2.koat | O(n²) | 5.31 s |
| KoAT-Suite/cousot9.koat | O(n²) | 3.71 s |
| KoAT-Suite/ex_paper1.c.koat | O(n²) | 13.30 s |
| KoAT-Suite/fib_exp_size.koat | EXP | 2.34 s |
| KoAT-Suite/fig5.koat | O(n) | 0.48 s |
| KoAT-Suite/fig6.koat | O(1) | 0.76 s |
| KoAT-Suite/fig7.koat | O(1) | 0.35 s |
| KoAT-Suite/geo_race.koat | O(n) | 0.55 s |
| KoAT-Suite/knuth_morris_pratt.c.koat | O(n) | 20.03 s |
| KoAT-Suite/leading.1.koat | O(n²) | 1.22 s |
| KoAT-Suite/leading.koat | O(n²) | 1.18 s |
| KoAT-Suite/multirace2.koat | O(n²) | 4.10 s |
| KoAT-Suite/neg_init_upd.koat | O(n) | 0.83 s |
| KoAT-Suite/nested_break.koat | Maybe | 2.32 s |
| KoAT-Suite/nested_rdwalk.koat | O(n) | 0.71 s |
| KoAT-Suite/nested_size.koat | O(n⁵) | 4.17 s |
| KoAT-Suite/nondet_countdown.koat | O(n) | 2.30 s |
| KoAT-Suite/prob_loop.koat | O(n) | 1.02 s |
| KoAT-Suite/prseq2.koat | O(n) | 0.81 s |
| KoAT-Suite/rank3.c.koat | O(n²) | 201.88 s |
| KoAT-Suite/rdseql2.koat | O(n) | 0.49 s |
| KoAT-Suite/realheapsort.koat | O(n²) | 186.19 s |
| KoAT-Suite/selectsort.koat | O(n²) | 158.19 s |
| KoAT-Suite/simple_nested.koat | O(n²) | 2.38 s |
| KoAT-Suite/spctrm.koat | O(n) | 18.87 s |
| KoAT-Suite/trunc_selectsort.koat | O(n²) | 183.13 s |
| KoAT-Suite/two_arrays2.koat | O(n) | 9.81 s |