General
This site provides supporting material for the paper Runtime Complexity Analysis of Logically Constrained Rewriting by Sarah Winkler and Georg Moser, submitted to LOPSTR 2020.Logically constrained rewrite systems (LCTRSs) are a versatile and efficient model of rewriting that can be used to model programs from various programming paradigms, as well as simplification systems in compilers and SMT solvers. In this paper, we investigate techniques to analyse the worst-case runtime complexity of LCTRSs. For that, we exploit the synergies between previously developed decomposition techniques for standard term rewriting by Avanzini et al. in conjunction with alternating time and size bound approximations for integer programs by Brockschmidt et al. and adapt these techniques suitably to LCTRSs. Furthermore, we provide novel modularization techniques to exploit loop bounds from recurrence equations which yield sublinear bounds. We have implemented the method in TCT and provide experimental data showing the viability of the method.
Examples
The following input files for TCT correspond to examples mentioned in the paper. The files are written in the KoAT format:- problems from the
Costa
benchmarks involving logarithmic bounds and divide-and-conquer patterns.
- mergesort (output O(n*log(n)))
- divide_and_conquer (output O(n))
- DivByTwo (output O(log(n)))
- direct_n_log_n (output O(log(n)))
- maxlength example from the introduction (output O(n))
Tool
The branch tct-lctrs of TCT can be obtained from this github repository. Please runstack build to create the executable.
This version of TCT requires yices 2.x.
Experiments
The following table compares TCT-LCTRS with other tools on the 689 integer transition systems (ITSs) considered in the evaluation of this paper by Brockschmidt et al:| TCT | TCT-ITS | KoAT | CoFloCo | PUBS | |
|---|---|---|---|---|---|
| FGPSF09/Beerendonk/01 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/Beerendonk/02 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/Beerendonk/03 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/Beerendonk/04 | O(1) | O(1) | O(1) | O(1) | O(log(n)) |
| FGPSF09/Beerendonk/05 | O(n) | O(n) | O(1) | O(n) | O(n) |
| FGPSF09/Beerendonk/06 | O(n) | O(n) | O(1) | O(n) | O(n) |
| FGPSF09/Beerendonk/07 | O(n) | O(n) | O(1) | O(n) | O(n) |
| FGPSF09/Beerendonk/08 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/Beerendonk/09 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/Beerendonk/10 | ? | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/Beerendonk/11 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/Beerendonk/13 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/Beerendonk/15 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/Beerendonk/16 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/Beerendonk/17 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/Beerendonk/18 | O(n) | O(n) | O(n) | O(n) | ? |
| FGPSF09/Beerendonk/19 | O(n) | O(n) | O(n) | O(n) | ? |
| FGPSF09/Beerendonk/20 | O(n) | O(n) | O(n) | O(n) | O(n * log(n)) |
| FGPSF09/Beerendonk/21 | O(n) | O(n) | O(n) | O(n) | O(n * log(n)) |
| FGPSF09/Beerendonk/22 | O(n) | O(n) | O(n) | O(n) | ? |
| FGPSF09/Beerendonk/23 | O(n) | O(n) | O(n) | O(n) | ? |
| FGPSF09/Beerendonk/24 | O(n) | O(n) | O(n) | O(n) | O(n * log(n)) |
| FGPSF09/CAV02/practical1 | O(n2) | O(n2) | O(n2) | O(n2) | O(n2) |
| FGPSF09/CAV02/practical2 | ? | ? | O(n) | O(n) | ? |
| FGPSF09/CAV05/c.05 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/ESOP08/abstractions | ? | ? | ? | ? | ? |
| FGPSF09/LICS04/c.01 | O(n2) | O(n2) | O(n2) | O(n2) | O(n * log(n)) |
| FGPSF09/LICS04/choice | ? | ? | ? | ? | ? |
| FGPSF09/PLDI06/c.03 | O(n) | O(n) | O(n) | O(n) | ? |
| FGPSF09/PLDI06/c.04 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/RTA08/round | ? | ? | ? | ? | ? |
| FGPSF09/SAS05/c.02 | O(n2) | O(n2) | O(n2) | O(n2) | O(n2) |
| FGPSF09/TACAS01/terminate | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/VMCAI04/complete1 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/VMCAI04/complete2 | ? | ? | O(1) | ? | ? |
| FGPSF09/VMCAI04/complete3 | O(n2) | O(n2) | O(n2) | O(n2) | O(n2) |
| FGPSF09/VMCAI04/complete4 | ? | ? | ? | ? | ? |
| FGPSF09/VMCAI05/poly1 | ? | ? | ? | ? | ? |
| FGPSF09/VMCAI05/poly2 | ? | ? | ? | ? | ? |
| FGPSF09/VMCAI05/poly3 | ? | ? | ? | ? | ? |
| FGPSF09/VMCAI05/poly4 | O(n) | O(n) | O(n) | O(n) | ? |
| FGPSF09/new/randomFullUpDown | ? | ? | ? | ? | ? |
| FGPSF09/new/unsatCond2 | ? | ? | ? | ? | ? |
| FGPSF09/patrs/div | O(n) | O(n) | O(n) | O(1) | O(n) |
| FGPSF09/patrs/increase1 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/patrs/increase2 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/patrs/increase3 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/patrs/increase4 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/patrs/pasta/a.01 | O(n2) | O(n2) | O(n2) | O(n2) | O(n2) |
| FGPSF09/patrs/pasta/a.02 | ? | ? | ? | ? | ? |
| FGPSF09/patrs/pasta/a.03 | O(n2) | O(n2) | O(n2) | O(n2) | O(n2) |
| FGPSF09/patrs/pasta/a.04 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/patrs/pasta/a.05 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/patrs/pasta/a.06 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/patrs/pasta/a.07 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/patrs/pasta/a.08 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/patrs/pasta/a.09 | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/patrs/pasta/a.10 | O(n) | O(n) | O(n) | O(n) | ? |
| FGPSF09/patrs/pasta/a.11 | O(n) | O(n) | O(n) | O(n) | ? |
| FGPSF09/patrs/random_full_no_wrap | O(n) | ? | O(n) | O(n) | ? |
| FGPSF09/patrs/random_no_wrap | O(n) | ? | O(n) | O(n) | O(n) |
| FGPSF09/patrs/sqrt | O(n) | O(n) | O(n) | O(n) | O(n) |
| FGPSF09/patrs/sumto_no_if | O(n) | O(n) | O(n) | O(n) | O(n) |
| KoAT-2013/sect1-lin | O(n) | O(n) | O(n) | O(n) | ? |
| KoAT-2013/sect1-quad | O(n2) | O(n2) | O(n2) | ? | ? |
| KoAT-2013/sect2 | O(n2) | O(n2) | O(n2) | O(n2) | ? |
| KoAT-2013/sect4-facSum | O(n2) | ? | O(n2) | O(n2) | O(n2) |
| KoAT-2013/sect5-len | O(n) | O(n) | O(n) | O(n) | O(n) |
| KoAT-2013/sect5-sumSum | O(n2) | O(n2) | O(n2) | O(n2) | O(n2) |
| KoAT-2014/adding-exp-growth1 | ? | ? | O(exp(n)) | ? | ? |
| KoAT-2014/adding-exp-growth2 | ? | ? | O(exp(n)) | ? | ? |
| KoAT-2014/adding-exp-growth3 | ? | ? | O(exp(n)) | ? | ? |
| KoAT-2014/exp-calls | ? | ? | O(exp(n)) | ? | O(exp(n)) |
| KoAT-2014/nesting-ex1 | O(n4) | O(n5) | O(n3) | ? | ? |
| KoAT-2014/scaling-doubly-exp-growth | ? | ? | O(exp(n)) | ? | ? |
| KoAT-2014/scaling-exp-growth | ? | ? | O(exp(n)) | ? | ? |
| SAS10/aaron2 | O(n) | O(n) | O(n) | ? | ? |
| SAS10/ackermann | O(n) | O(n) | O(n) | O(n) | O(n) |
| SAS10/ax | O(n2) | O(n2) | O(n2) | O(n2) | ? |
| SAS10/complex | O(n) | O(n) | O(n) | ? | ? |
| SAS10/counterex1 | O(n3) | O(n3) | ? | ? | ? |
| SAS10/cousot9 | O(n2) | O(n2) | O(n2) | ? | ? |
| SAS10/determinant | O(n3) | O(n3) | O(n3) | O(n3) | O(n3) |
| SAS10/easy1 | O(n) | O(n) | O(1) | ? | ? |
| SAS10/easy2 | O(n) | O(n) | O(n) | O(n) | O(n) |
| SAS10/exmini | O(n) | O(n) | O(n) | O(n) | O(n) |
| SAS10/gcd | O(n) | O(n) | O(n) | ? | ? |
| SAS10/insertsort | O(n2) | O(n2) | O(n2) | O(n2) | O(n2) |
| SAS10/loops | O(n2) | O(n2) | O(n2) | ? | ? |
| SAS10/maccarthy91 | O(n) | O(n) | O(n) | ? | ? |
| SAS10/nd_loop | O(1) | O(1) | O(1) | O(1) | O(1) |
| SAS10/ndecr | O(n) | O(n) | O(n) | O(n) | O(n) |
| SAS10/nestedLoop | O(n2) | O(n2) | O(n2) | ? | ? |
| SAS10/perfect | O(n2) | O(n2) | O(n2) | O(n2) | ? |
| SAS10/random1d | O(n) | O(n) | O(n) | O(n) | O(n) |
| SAS10/random2d | O(n) | O(n) | O(n) | O(n) | O(n) |
| SAS10/realbubble | O(n2) | O(n2) | O(n2) | O(n2) | ? |
| SAS10/realheapsort | ? | O(n2) | O(n2) | ? | ? |
| SAS10/realselect | O(n) | O(n) | O(n) | O(1) | O(n) |
| SAS10/realshellsort | O(n3) | O(n3) | O(n3) | ? | ? |
| SAS10/relation1 | O(1) | O(1) | O(1) | O(1) | O(1) |
| SAS10/rsd | O(n2) | O(n2) | O(n2) | ? | ? |
| SAS10/sipmabubble | O(n2) | O(n3) | O(n2) | ? | ? |
| SAS10/speedFails4 | O(n) | O(n) | O(n) | ? | ? |
| SAS10/speedpldi2 | O(n) | O(n) | O(n) | O(n) | O(n) |
| SAS10/speedpldi3 | O(n2) | O(n2) | O(n2) | O(n2) | ? |
| SAS10/speedpldi4 | O(n) | O(n) | O(n) | O(n) | O(n) |
| SAS10/terminate | O(n) | O(n) | O(n) | O(n) | O(n) |
| SAS10/wcet1 | O(n) | O(n) | O(n) | O(n) | O(n) |
| SAS10/wcet2 | O(n) | O(n) | O(n) | ? | ? |
| SAS10/while2 | O(n2) | O(n2) | O(n2) | O(n2) | ? |
| SAS10/wise | O(n) | O(n) | O(n) | ? | ? |
| T2/1 | ? | ? | ? | ? | ? |
| T2/1394-fail | ? | ? | ? | ? | ? |
| T2/1394-succeed | ? | ? | ? | ? | ? |
| T2/1394complete-fail | ? | ? | ? | ? | ? |
| T2/1394complete-succeed | ? | ? | ? | ? | ? |
| T2/2 | ? | ? | ? | ? | ? |
| T2/232 | O(n2) | O(n2) | O(n2) | O(n2) | ? |
| T2/241 | O(n2) | O(n2) | O(n2) | O(n2) | ? |
| T2/3 | ? | ? | ? | ? | ? |
| T2/5 | ? | ? | ? | ? | ? |
| T2/6 | ? | ? | ? | ? | ? |
| T2/7 | ? | ? | ? | ? | ? |
| T2/Loop | O(n) | ? | O(n) | ? | ? |
| T2/a.10.c | O(n) | O(n2) | O(n2) | O(n) | ? |
| T2/acqrel-fail | ? | ? | ? | ? | ? |
| T2/afagp-fail | ? | ? | ? | ? | ? |
| T2/afagx1 | ? | ? | ? | ? | ? |
| T2/agafp | ? | ? | ? | ? | ? |
| T2/apchild-accepted-fail | ? | ? | ? | ? | ? |
| T2/apchild-accepted | ? | ? | ? | ? | ? |
| T2/apchild-live | ? | ? | ? | ? | ? |
| T2/apchildlive-succeed | ? | ? | ? | ? | ? |
| T2/array | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/array1 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/array2 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/array3 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/array_free | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/array_init | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/array_init_assign | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ase_example | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf10 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf11 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf12 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf13 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf14 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf15 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf16 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf17 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf18 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf19 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf20 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf5 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf6 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf7 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf8 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bf9 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bio | ? | ? | ? | ? | ? |
| T2/bitcount16 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bitcount32 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/broydn.c.i.broydn.pl.t2.fixed | ? | ? | ? | ? | ? |
| T2/broydn.c.i.broydn.pl.t2.nor.t2.rlgfixed | ? | ? | ? | ? | ? |
| T2/broydn | ? | ? | ? | ? | ? |
| T2/brp | ? | ? | ? | ? | ? |
| T2/brp_withassume | ? | ? | ? | ? | ? |
| T2/bs | ? | ? | ? | ? | ? |
| T2/bsort100 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/bubbleSort | O(n2) | O(n2) | O(n2) | O(n2) | O(n2) |
| T2/bubblesort_inner_loop | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/buggyNonTermLoop | ? | ? | ? | ? | ? |
| T2/byron-1 | O(n) | ? | O(n) | O(n) | ? |
| T2/byron-2 | ? | ? | ? | ? | ? |
| T2/byron-3 | ? | ? | ? | ? | ? |
| T2/byron-4 | O(n) | O(n) | O(n) | O(n) | ? |
| T2/cfg | ? | ? | ? | ? | ? |
| T2/cnt | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/collatz | ? | ? | ? | ? | ? |
| T2/complex_guard | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/constants | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/consts1 | O(1) | O(1) | O(1) | O(1) | ? |
| T2/consts1nt | ? | ? | ? | ? | ? |
| T2/consts2 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/consts2nt | ? | ? | ? | ? | ? |
| T2/consts3 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/consts3nt | ? | ? | ? | ? | ? |
| T2/consts4 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/consts4nt | ? | ? | ? | ? | ? |
| T2/consts5 | O(1) | O(1) | O(1) | O(1) | ? |
| T2/consts5nt | ? | ? | ? | ? | ? |
| T2/cover | ? | O(1) | O(1) | ? | ? |
| T2/crc | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/create | ? | ? | ? | ? | ? |
| T2/create_seg | ? | ? | ? | ? | ? |
| T2/create_via_tmps | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/ctl | ? | ? | ? | ? | ? |
| T2/curious | ? | ? | ? | ? | ? |
| T2/curious4 | ? | ? | ? | ? | ? |
| T2/d | ? | ? | ? | ? | ? |
| T2/db2 | ? | ? | ? | ? | ? |
| T2/db3 | ? | ? | ? | ? | ? |
| T2/dead.neg-st88b-succeed | ? | ? | ? | ? | ? |
| T2/destroy | ? | ? | ? | ? | ? |
| T2/destroy_seg | ? | ? | ? | ? | ? |
| T2/destroy_seg_leak | ? | ? | ? | ? | ? |
| T2/disj_nightmare_abi | O(1) | O(1) | O(1) | O(1) | ? |
| T2/dropbuf-live | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/dropbuf | ? | ? | ? | ? | ? |
| T2/dsa_test | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/dsa_test1 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/dsa_test10 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/dsa_test11 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/dsa_test12 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/dsa_test13 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/dsa_test15 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/dsa_test4 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/dsa_test5 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/dsa_test6 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/dsa_test8 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/dsa_test9 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/dummy | ? | ? | ? | ? | ? |
| T2/e-1394complete-succeed | ? | ? | ? | ? | ? |
| T2/e-acqrel-fail | ? | ? | ? | ? | ? |
| T2/e-acqrel-succeed | ? | ? | ? | ? | ? |
| T2/e-pgarch-fail | ? | ? | ? | ? | ? |
| T2/e-pgarch-succeed | ? | ? | ? | ? | ? |
| T2/e-popl07-fail | ? | ? | ? | ? | ? |
| T2/edn | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/efegp | ? | ? | ? | ? | ? |
| T2/elmhes.c.i.elmhes.pl.t2.fixed | ? | ? | O(n2) | ? | ? |
| T2/elmhes.c.i.elmhes.pl.t2.nor.t2.rlgfixed | ? | ? | O(n2) | ? | ? |
| T2/elmhes | ? | ? | O(n2) | ? | ? |
| T2/eric | ? | ? | ? | O(n) | ? |
| T2/eric1 | ? | ? | ? | O(n2) | ? |
| T2/eric2 | ? | ? | ? | ? | ? |
| T2/eric3 | ? | ? | ? | ? | ? |
| T2/ex1 | ? | ? | ? | ? | ? |
| T2/ex10 | ? | ? | ? | ? | ? |
| T2/ex11 | ? | ? | ? | ? | ? |
| T2/ex12 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex13 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex14 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex15 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex16 | ? | ? | ? | ? | ? |
| T2/ex17 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex18 | O(1) | O(1) | ? | O(1) | ? |
| T2/ex19 | ? | ? | ? | ? | ? |
| T2/ex2 | ? | ? | ? | ? | ? |
| T2/ex20 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex21 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex22 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex23 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex26 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex27 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex29 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex3 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex30 | ? | ? | ? | ? | ? |
| T2/ex31 | ? | ? | ? | ? | ? |
| T2/ex32 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex33 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex34 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex36 | ? | ? | ? | ? | ? |
| T2/ex37 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex4 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex40 | ? | ? | ? | ? | ? |
| T2/ex6 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex7 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/ex8 | ? | ? | ? | ? | ? |
| T2/ex9 | ? | ? | ? | ? | ? |
| T2/example | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/fake-succeed | ? | ? | ? | ? | ? |
| T2/fast_poll | ? | ? | ? | ? | ? |
| T2/fdct | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/fermat | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/fibcall | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/fir | ? | ? | ? | ? | ? |
| T2/firewire | ? | ? | ? | ? | ? |
| T2/flipflop | ? | ? | ? | ? | ? |
| T2/fourn.c.i.fourn.pl.t2.fixed | O(n) | ? | O(n) | ? | ? |
| T2/fourn.c.i.fourn.pl.t2.nor.t2.rlgfixed | ? | ? | ? | ? | ? |
| T2/fourn | ? | ? | ? | ? | ? |
| T2/fuhs-inflasso | O(n2) | O(n3) | O(n2) | O(n2) | ? |
| T2/fun1 | ? | ? | ? | ? | ? |
| T2/fun10 | ? | ? | ? | ? | ? |
| T2/fun10b | ? | ? | ? | ? | ? |
| T2/fun11 | ? | ? | ? | ? | ? |
| T2/fun1b | ? | ? | ? | ? | ? |
| T2/fun2 | O(n) | ? | O(n) | ? | ? |
| T2/fun2b | ? | ? | ? | ? | ? |
| T2/fun3 | O(n) | ? | O(n) | ? | ? |
| T2/fun4-alt | O(n) | O(n) | O(1) | O(n) | ? |
| T2/fun4 | O(n) | O(n) | O(1) | O(n) | ? |
| T2/fun5 | ? | ? | ? | ? | ? |
| T2/fun6 | ? | ? | ? | ? | ? |
| T2/fun7 | ? | ? | ? | ? | ? |
| T2/fun8 | ? | O(1) | O(1) | O(1) | ? |
| T2/fun9 | ? | ? | ? | ? | ? |
| T2/graycode | O(1) | O(1) | O(1) | ? | ? |
| T2/heidy1 | ? | ? | ? | ? | ? |
| T2/heidy10 | ? | ? | ? | ? | ? |
| T2/heidy2 | ? | ? | ? | ? | ? |
| T2/heidy3 | ? | ? | ? | ? | ? |
| T2/heidy5 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/heidy6 | ? | ? | ? | ? | ? |
| T2/heidy7-simple | ? | ? | ? | ? | ? |
| T2/heidy7 | ? | ? | ? | ? | ? |
| T2/heidy8 | ? | ? | ? | ? | ? |
| T2/heidy9 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/hongyi1 | ? | ? | O(n) | ? | O(n) |
| T2/hqr.c.i.hqr.pl.t2.fixed | ? | ? | ? | ? | ? |
| T2/hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed | ? | ? | ? | ? | ? |
| T2/hqr | ? | ? | ? | ? | ? |
| T2/huh | ? | ? | ? | ? | ? |
| T2/iecs | O(n) | ? | O(n) | O(n) | ? |
| T2/insertsort | ? | ? | ? | ? | ? |
| T2/intSqRoot | ? | ? | ? | ? | ? |
| T2/invgen | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/jacobi.c.i.jacobi.pl.t2.fixed | O(n) | ? | O(n) | ? | ? |
| T2/jacobi.c.i.jacobi.pl.t2.nor.t2.rlgfixed | ? | ? | O(n) | ? | ? |
| T2/jacobi | ? | ? | O(n) | ? | ? |
| T2/janne_complex | ? | ? | ? | ? | ? |
| T2/jfdctint | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/loop3 | ? | ? | O(1) | ? | ? |
| T2/loop_on_input | ? | ? | O(1) | O(1) | ? |
| T2/ludcmp.c.i.ludcmp.pl.t2.fixed | ? | ? | O(n) | ? | ? |
| T2/ludcmp.c.i.ludcmp.pl.t2.nor.t2.rlgfixed | ? | ? | O(n) | ? | ? |
| T2/ludcmp | ? | ? | O(n) | ? | ? |
| T2/magic | ? | ? | ? | ? | ? |
| T2/matmul | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/matmult | O(n) | O(1) | O(1) | O(1) | O(1) |
| T2/matrixsqrt | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/mc91 | ? | ? | ? | ? | ? |
| T2/mc91test | ? | ? | ? | ? | ? |
| T2/minmax | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/n-1 | ? | ? | ? | ? | ? |
| T2/n-10 | ? | ? | ? | ? | ? |
| T2/n-12 | ? | ? | ? | ? | ? |
| T2/n-12a | ? | ? | ? | ? | ? |
| T2/n-13 | ? | ? | ? | ? | ? |
| T2/n-14 | ? | ? | ? | ? | ? |
| T2/n-15 | ? | ? | ? | ? | ? |
| T2/n-15a | ? | ? | ? | ? | ? |
| T2/n-16 | ? | ? | ? | ? | ? |
| T2/n-16a | ? | ? | ? | ? | ? |
| T2/n-17 | ? | ? | ? | ? | ? |
| T2/n-18 | ? | ? | ? | ? | ? |
| T2/n-18a | ? | ? | ? | ? | ? |
| T2/n-1c | ? | ? | ? | ? | ? |
| T2/n-1d | ? | ? | ? | ? | ? |
| T2/n-20 | ? | ? | ? | ? | ? |
| T2/n-21 | ? | ? | ? | ? | ? |
| T2/n-3 | ? | ? | ? | ? | ? |
| T2/n-32 | ? | ? | ? | ? | ? |
| T2/n-33 | ? | ? | ? | ? | ? |
| T2/n-36 | ? | ? | ? | ? | ? |
| T2/n-37 | ? | ? | ? | ? | ? |
| T2/n-3a | ? | ? | ? | ? | ? |
| T2/n-4 | ? | ? | ? | ? | ? |
| T2/n-40 | ? | ? | ? | ? | ? |
| T2/n-46 | ? | ? | ? | ? | ? |
| T2/n-48 | ? | ? | ? | ? | ? |
| T2/n-5 | ? | ? | ? | ? | ? |
| T2/n-6 | ? | ? | ? | ? | ? |
| T2/n-6a | ? | ? | ? | ? | ? |
| T2/n-7 | ? | ? | ? | ? | ? |
| T2/n-8 | ? | ? | ? | ? | ? |
| T2/n-8a | ? | ? | ? | ? | ? |
| T2/n-9 | ? | ? | ? | ? | ? |
| T2/n_firewire_instrumented-PP | ? | ? | ? | ? | ? |
| T2/nakata | ? | ? | ? | ? | ? |
| T2/nakata_withassume | ? | ? | ? | ? | ? |
| T2/ndes | ? | ? | O(1) | ? | ? |
| T2/neg-1394complete-fail | ? | ? | ? | ? | ? |
| T2/neg-1394complete-succeed | ? | ? | ? | ? | ? |
| T2/neg-e-1394complete-fail | ? | ? | ? | ? | ? |
| T2/neg-e-1394complete-succeed | ? | ? | ? | ? | ? |
| T2/neg-e-acqrel-fail | ? | ? | ? | ? | ? |
| T2/neg-e-acqrel-succeed | ? | ? | ? | ? | ? |
| T2/neg-e-pgarch-fail | ? | ? | ? | ? | ? |
| T2/neg-e-pgarch-succeed | ? | ? | ? | ? | ? |
| T2/neg-e-popl07-succeed | ? | ? | ? | ? | ? |
| T2/neg-pgarch-succeed | ? | ? | ? | ? | ? |
| T2/neg-popl07-fail | ? | ? | ? | ? | ? |
| T2/neg-popl07-succeed | ? | ? | ? | ? | ? |
| T2/neg-smagilla-fail | ? | ? | ? | ? | ? |
| T2/neg-smagilla-succeed | ? | ? | ? | ? | ? |
| T2/nested | ? | ? | ? | ? | ? |
| T2/nested2 | ? | ? | ? | ? | ? |
| T2/new_ex | ? | ? | ? | ? | ? |
| T2/non_term | ? | ? | ? | ? | ? |
| T2/ns | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/oct_vs_subpoly | ? | ? | ? | ? | ? |
| T2/p-1 | ? | ? | ? | ? | ? |
| T2/p-10 | ? | ? | ? | ? | ? |
| T2/p-12 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-13 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/p-14 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-15 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-16 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-18 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-19 | ? | ? | ? | ? | ? |
| T2/p-19a | ? | ? | ? | ? | ? |
| T2/p-1a | ? | ? | ? | ? | ? |
| T2/p-1b | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-1c | ? | ? | ? | ? | ? |
| T2/p-1d | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-20 | ? | ? | ? | ? | ? |
| T2/p-21 | O(n) | O(n) | O(n) | O(n) | ? |
| T2/p-22 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-3 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-32 | ? | ? | ? | ? | ? |
| T2/p-33 | ? | ? | ? | ? | ? |
| T2/p-34 | ? | ? | ? | ? | ? |
| T2/p-36 | ? | ? | ? | ? | ? |
| T2/p-37 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/p-4 | O(n2) | O(n2) | O(n2) | O(n) | ? |
| T2/p-40 | ? | ? | ? | ? | ? |
| T2/p-41 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/p-42 | O(n) | O(n) | O(n) | O(n) | ? |
| T2/p-43-terminate | ? | ? | ? | ? | ? |
| T2/p-43 | ? | ? | ? | ? | ? |
| T2/p-44 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-45 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-46 | ? | ? | ? | ? | ? |
| T2/p-49 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-5 | ? | ? | ? | ? | ? |
| T2/p-52 | ? | ? | ? | ? | ? |
| T2/p-53 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/p-55 | O(n) | O(n2) | O(n2) | O(n) | ? |
| T2/p-56 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-58 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/p-6 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-60 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/p-61 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/p-63 | O(n) | ? | O(n) | O(n) | ? |
| T2/p-7 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-7b | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/p-8 | ? | ? | ? | ? | ? |
| T2/p-9 | ? | ? | ? | ? | ? |
| T2/pearl-necklace | O(n) | O(n) | O(n) | O(n) | ? |
| T2/pentagon | ? | ? | ? | ? | ? |
| T2/pgarch | ? | ? | ? | ? | ? |
| T2/pldi | ? | ? | O(n2) | O(n2) | ? |
| T2/polling.bug | ? | ? | ? | ? | ? |
| T2/polling | ? | ? | ? | ? | ? |
| T2/polyrank1 | ? | ? | ? | ? | ? |
| T2/polyrank2 | ? | ? | ? | ? | ? |
| T2/polyrank3 | ? | ? | ? | ? | ? |
| T2/polyrank4 | ? | ? | ? | ? | ? |
| T2/polyrank5 | ? | ? | ? | ? | ? |
| T2/polyrank6 | ? | ? | ? | ? | ? |
| T2/polyrank7 | ? | ? | ? | ? | ? |
| T2/popl07-fail | ? | ? | ? | ? | ? |
| T2/popl07-succeed | ? | ? | ? | ? | ? |
| T2/print | ? | ? | ? | ? | ? |
| T2/qrdcmp.c.i.qrdcmp.pl.t2.fixed | O(n) | ? | O(n) | ? | ? |
| T2/qrdcmp.c.i.qrdcmp.pl.t2.nor.t2.rlgfixed | O(n) | O(n) | O(n) | ? | ? |
| T2/qrdcmp | O(n) | O(n) | O(n) | ? | ? |
| T2/queens | ? | ? | O(1) | ? | ? |
| T2/queue_1 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/queue_10 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/queue_100 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/queue_1000 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/randomwalk | ? | ? | ? | ? | ? |
| T2/randomwalk_withassume | ? | ? | ? | ? | ? |
| T2/refine_disj_problem | ? | ? | ? | ? | ? |
| T2/rev_nt2 | ? | ? | ? | ? | ? |
| T2/rev_nt3 | ? | ? | ? | ? | ? |
| T2/rev_nt4 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/reverse | ? | ? | ? | ? | ? |
| T2/reverse_div4 | ? | ? | ? | ? | ? |
| T2/reverse_seg_cyclic | O(n) | O(n) | O(n) | ? | ? |
| T2/rewrite | ? | ? | ? | ? | ? |
| T2/rlft3.c.i.rlft3.pl.t2.fixed | O(n) | ? | O(n) | ? | ? |
| T2/rlft3 | O(n) | O(n) | O(n) | ? | ? |
| T2/s1-saved | ? | ? | ? | ? | ? |
| T2/s3-work | ? | ? | ? | ? | ? |
| T2/sas1 | O(n2) | O(n2) | O(n) | O(n) | ? |
| T2/sas2 | ? | ? | ? | O(n) | ? |
| T2/select | ? | ? | ? | ? | ? |
| T2/selectSort | O(n3) | O(n2) | O(n2) | O(n2) | O(n2) |
| T2/send-more-money | O(1) | O(1) | O(1) | ? | ? |
| T2/seq | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/seq2 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/sequential_swap | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/simple | ? | ? | ? | ? | ? |
| T2/simpleWhile | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/simple_array_inversion | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/simple_control_on_input | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/simple_double_free | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/simple_fail | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/simple_pre | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/simple_pre1 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/simple_pre2 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/simple_pre3 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/simple_swap_call | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/slayer-1-filtered | ? | ? | ? | ? | ? |
| T2/slayer-1-rf | ? | ? | ? | ? | ? |
| T2/slayer-2-filtered | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/slayer-3-filtered | ? | ? | ? | ? | ? |
| T2/slayer-3-new | ? | ? | ? | ? | ? |
| T2/slayer-3 | ? | ? | ? | ? | ? |
| T2/slayer-4-filtered | ? | ? | ? | ? | ? |
| T2/slayer-n1-filtered | ? | ? | ? | ? | ? |
| T2/slayer-n1 | ? | ? | ? | ? | ? |
| T2/slayer-n2-filtered | ? | ? | ? | ? | ? |
| T2/slayer-n2 | ? | ? | ? | ? | ? |
| T2/slayer-n3-filtered | O(1) | O(1) | O(1) | ? | O(1) |
| T2/slayer-n5-filtered | ? | ? | ? | ? | ? |
| T2/smagilla-succeed | ? | ? | ? | ? | ? |
| T2/smagillb-succeed | ? | ? | ? | ? | ? |
| T2/smagillc-fail | ? | ? | ? | ? | ? |
| T2/smagillc-succeed | ? | ? | ? | ? | ? |
| T2/sort | O(1) | O(1) | O(1) | ? | O(1) |
| T2/spctrm.c.i.spctrm.pl.t2.fixed | O(n) | ? | O(n) | ? | ? |
| T2/spctrm.c.i.spctrm.pl.t2.nor.t2.rlgfixed | O(n) | O(n) | O(n) | ? | ? |
| T2/spctrm | O(n) | O(n) | O(n) | ? | ? |
| T2/spiral | ? | O(n2) | O(n2) | O(n) | ? |
| T2/st88.bug | ? | ? | ? | ? | ? |
| T2/st88 | ? | ? | ? | ? | ? |
| T2/statemate | ? | ? | ? | ? | ? |
| T2/stored | ? | ? | ? | ? | ? |
| T2/streamserver-succeed | ? | ? | ? | ? | ? |
| T2/streamserver.bug | ? | ? | ? | ? | ? |
| T2/subpoly_crash | ? | ? | ? | ? | ? |
| T2/sudoku | ? | ? | ? | ? | ? |
| T2/sumit | ? | ? | ? | O(n) | ? |
| T2/svdcmp.c.i.svdcmp.pl.t2.fixed | ? | ? | ? | ? | ? |
| T2/svdcmp.c.i.svdcmp.pl.t2.nor.t2.rlgfixed | ? | ? | ? | ? | ? |
| T2/svdcmp | ? | ? | ? | ? | ? |
| T2/toeplz.c.i.toeplz.pl.t2.fixed | O(n2) | ? | O(n2) | O(n2) | ? |
| T2/toeplz.c.i.toeplz.pl.t2.nor.t2.rlgfixed | ? | ? | ? | ? | ? |
| T2/toeplz | ? | ? | ? | ? | ? |
| T2/tqli.c.i.tqli.pl.t2.fixed | ? | ? | ? | ? | ? |
| T2/tqli.c.i.tqli.pl.t2.nor.t2.rlgfixed | ? | ? | ? | ? | ? |
| T2/tqli | ? | ? | ? | ? | ? |
| T2/traverse | ? | ? | ? | ? | ? |
| T2/traverse2 | ? | ? | ? | ? | ? |
| T2/traverse_seg | ? | ? | ? | ? | ? |
| T2/traverse_seg2 | ? | ? | ? | ? | ? |
| T2/traverse_twice | ? | ? | ? | ? | ? |
| T2/two_arrays | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/two_arrays1 | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/two_arrays2 | O(n) | O(n) | O(n) | O(n) | O(n) |
| T2/two_arrays6 | O(n2) | O(n) | O(n) | O(n) | O(n) |
| T2/ud | O(1) | O(1) | O(1) | O(1) | ? |
| T2/vmcai_bytes | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/vmcai_struct | O(1) | O(1) | O(1) | O(1) | O(1) |
| T2/w1 | ? | ? | ? | ? | ? |
| T2/w2_nt | ? | ? | ? | ? | ? |
| T2/walk | ? | ? | ? | ? | ? |
| T2/wrong_loop | ? | ? | ? | ? | ? |
| T2/wtf | O(n) | ? | O(n) | ? | ? |
| T2/zeroconf | ? | ? | ? | ? | ? |
| T2/zeroconf_withassume | ? | ? | ? | ? | ? |
| c-examples/ABC/ex01 | O(n) | O(n) | O(n) | O(n) | O(n) |
| c-examples/ABC/ex02 | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/ABC/ex03 | O(n6) | O(n4) | O(n6) | O(n4) | O(n) |
| c-examples/ABC/ex04 | ? | ? | ? | ? | ? |
| c-examples/ABC/ex05 | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/ABC/ex06 | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/ABC/ex07 | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/ABC/ex08 | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/ABC/ex09 | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/ABC/ex10 | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/ABC/ex11 | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/ABC/ex12 | O(n2) | O(n2) | O(n2) | O(n) | O(n) |
| c-examples/ABC/ex13 | O(n3) | O(n3) | O(n4) | O(n3) | O(n) |
| c-examples/ABC/ex14 | O(n9) | O(n6) | O(n8) | O(n4) | O(n) |
| c-examples/ABC/ex15 | ? | ? | ? | ? | O(n) |
| c-examples/Loopus/Example1 | O(n) | ? | O(n) | O(n) | ? |
| c-examples/Loopus/Example2 | ? | ? | ? | O(n) | ? |
| c-examples/Loopus/Example3 | O(n) | ? | O(n) | O(n) | ? |
| c-examples/Rank/ex1 | O(n3) | ? | O(n2) | O(n2) | ? |
| c-examples/Rank/ex2 | ? | ? | O(n) | O(n2) | O(n) |
| c-examples/Rank/ex3 | ? | ? | O(n) | O(n2) | ? |
| c-examples/SPEED/CAV09/ex1 | O(n) | O(n) | O(n) | O(n) | ? |
| c-examples/SPEED/CAV09/ex2 | O(n2) | O(n2) | O(n2) | O(n2) | ? |
| c-examples/SPEED/CAV09/ex3 | O(n) | O(n) | O(n) | O(n) | ? |
| c-examples/SPEED/PLDI09/Example2 | O(n) | ? | O(n) | O(n) | ? |
| c-examples/SPEED/PLDI09/Example3 | O(n3) | ? | O(n2) | O(n2) | ? |
| c-examples/SPEED/PLDI09/Example4 | ? | ? | O(n2) | ? | ? |
| c-examples/SPEED/PLDI09/Example5 | O(n) | ? | O(n2) | O(n) | ? |
| c-examples/SPEED/PLDI09/Example6 | O(n) | O(n) | O(n) | O(n2) | ? |
| c-examples/SPEED/PLDI09/NestedLoop | O(n3) | ? | O(n2) | O(n2) | ? |
| c-examples/SPEED/PLDI09/cyclic | ? | ? | ? | O(n) | ? |
| c-examples/SPEED/PLDI10/Ex1 | ? | ? | ? | O(n2) | ? |
| c-examples/SPEED/PLDI10/Ex2 | ? | ? | ? | ? | ? |
| c-examples/SPEED/PLDI10/Ex3 | ? | ? | ? | ? | ? |
| c-examples/SPEED/PLDI10/Ex4 | O(n) | O(n) | O(n) | O(n) | ? |
| c-examples/SPEED/PLDI10/Ex5 | ? | ? | ? | ? | ? |
| c-examples/SPEED/PLDI10/Ex6 | O(n) | O(n) | O(n) | O(n) | ? |
| c-examples/SPEED/PLDI10/Ex7 | ? | ? | ? | O(n) | ? |
| c-examples/SPEED/POPL09/Dis1 | O(n2) | O(n) | O(n) | O(n) | ? |
| c-examples/SPEED/POPL09/Dis2 | O(n) | O(n) | O(n) | O(n) | ? |
| c-examples/SPEED/POPL09/NestedMultiple | O(n2) | O(n) | ? | O(n) | O(n) |
| c-examples/SPEED/POPL09/NestedMultipleDep | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/SPEED/POPL09/NestedSingle | O(n) | O(n) | O(n) | O(n) | ? |
| c-examples/SPEED/POPL09/SequentialSingle | O(n) | O(n) | O(n) | O(n) | O(n) |
| c-examples/SPEED/POPL09/SimpleMultiple | O(n2) | O(n) | O(n) | O(n) | ? |
| c-examples/SPEED/POPL09/SimpleMultipleDep | O(n2) | O(n2) | O(n2) | O(n2) | ? |
| c-examples/SPEED/POPL09/SimpleSingle | O(n) | O(n) | O(n) | O(n) | O(n) |
| c-examples/SPEED/POPL09/SimpleSingle2 | O(n) | O(n) | O(n) | O(n) | ? |
| c-examples/WTC/aaron2 | O(n) | O(n) | O(n) | O(n) | O(n) |
| c-examples/WTC/ax | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/WTC/complex | ? | ? | ? | ? | ? |
| c-examples/WTC/counterex1b | ? | ? | ? | ? | ? |
| c-examples/WTC/cousot9 | ? | ? | ? | ? | ? |
| c-examples/WTC/easy1 | O(1) | O(1) | O(1) | O(1) | O(1) |
| c-examples/WTC/easy2 | O(n) | O(n) | O(n) | O(n) | O(n) |
| c-examples/WTC/exmini | O(n) | O(n) | O(n) | O(n) | O(n) |
| c-examples/WTC/gcd | ? | ? | ? | O(n) | ? |
| c-examples/WTC/insertsort | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/WTC/loops | ? | ? | O(n2) | O(n2) | O(n) |
| c-examples/WTC/nd_loop | O(1) | O(1) | O(1) | O(1) | O(1) |
| c-examples/WTC/ndecr | O(n) | O(n) | O(n) | O(n) | O(n) |
| c-examples/WTC/nestedLoop | O(n2) | O(n2) | ? | O(n2) | ? |
| c-examples/WTC/perfect | ? | ? | O(n2) | O(n2) | O(n) |
| c-examples/WTC/random1d | O(n) | O(n) | O(n) | O(n) | O(n) |
| c-examples/WTC/random2d | O(n) | O(n) | O(n) | O(n) | O(n) |
| c-examples/WTC/realbubble | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/WTC/realheapsort | ? | ? | O(n2) | ? | O(n) |
| c-examples/WTC/realheapsort_step1 | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/WTC/realheapsort_step2 | ? | ? | O(n2) | ? | O(n) |
| c-examples/WTC/realselect | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/WTC/realshellsort | ? | ? | O(n3) | ? | O(log(n)) |
| c-examples/WTC/rsd | O(n2) | ? | O(n2) | O(n2) | ? |
| c-examples/WTC/sipma91 | O(n) | ? | O(n2) | O(n) | ? |
| c-examples/WTC/sipmabubble | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/WTC/speedFails4 | ? | ? | ? | ? | ? |
| c-examples/WTC/speedpldi2 | ? | ? | O(n) | O(n) | ? |
| c-examples/WTC/speedpldi3 | O(n2) | O(n2) | O(n2) | O(n2) | ? |
| c-examples/WTC/speedpldi4 | O(n) | ? | O(n) | O(n) | ? |
| c-examples/WTC/terminate | O(n) | O(n) | O(n) | O(n) | O(n) |
| c-examples/WTC/wcet1 | O(n) | O(n) | O(n) | O(n) | O(n) |
| c-examples/WTC/wcet2 | O(n) | O(n) | O(n) | O(n) | O(n) |
| c-examples/WTC/while2 | O(n2) | O(n2) | O(n2) | O(n2) | O(n) |
| c-examples/WTC/wise | O(n) | ? | O(n) | O(n) | ? |
| costa/RAML/bitvectors | ? | ? | O(n2) | O(n2) | O(n2) |
| costa/RAML/cleavermmult | ? | ? | O(n3) | O(n3) | O(n3) |
| costa/RAML/duplicates | O(n) | ? | O(n) | O(n) | O(n) |
| costa/RAML/dyade | O(n2) | ? | O(n2) | O(n2) | O(n2) |
| costa/RAML/eratosthenes | O(n2) | ? | O(n2) | O(n2) | O(n2) |
| costa/RAML/insertionsort | O(n2) | ? | O(n2) | O(n2) | O(n2) |
| costa/RAML/lcs | ? | ? | O(n2) | O(n2) | O(n2) |
| costa/RAML/listsort | O(n3) | ? | O(n3) | O(n3) | O(n3) |
| costa/RAML/matrix | O(n2) | ? | O(n3) | O(n3) | O(n3) |
| costa/RAML/mergesort | O(n * log(n)) | ? | O(exp(n)) | ? | O(n2) |
| costa/RAML/minsort | O(n2) | ? | O(n2) | O(n2) | O(n2) |
| costa/RAML/quicksort | ? | ? | O(exp(n)) | ? | O(exp(n)) |
| costa/RAML/rationalPotential | O(n) | O(n) | O(n) | O(n) | O(n) |
| costa/jvm-cost/ArrayReverse | O(n) | ? | O(exp(n)) | O(n) | O(n) |
| costa/jvm-cost/BST | ? | ? | O(exp(n)) | ? | O(exp(n)) |
| costa/jvm-cost/Concat | O(n) | ? | O(n) | O(n) | O(n) |
| costa/jvm-cost/Cons | O(n) | ? | O(n) | O(n) | O(n) |
| costa/jvm-cost/Delete | ? | ? | O(exp(n)) | O(n2) | O(n2) |
| costa/jvm-cost/DetEval | ? | ? | ? | O(n3) | O(n3) |
| costa/jvm-cost/DivByTwo | O(log(n)) | ? | O(n) | O(n) | O(log(n)) |
| costa/jvm-cost/EvenDigits | O(n * log(n)) | ? | O(n) | O(n) | O(n * log(n)) |
| costa/jvm-cost/EvenDigitsNew | ? | ? | O(n2) | O(n2) | O(n * log(n)) |
| costa/jvm-cost/FactSum | O(n2) | ? | O(exp(n)) | O(n2) | O(n2) |
| costa/jvm-cost/FactSumNew | O(n2) | ? | O(n2) | O(n2) | O(n2) |
| costa/jvm-cost/Factorial | O(n) | ? | O(n) | O(n) | O(n) |
| costa/jvm-cost/Fibonacci | ? | ? | O(exp(n)) | ? | O(exp(n)) |
| costa/jvm-cost/FibonacciNew | ? | ? | O(exp(n)) | ? | ? |
| costa/jvm-cost/Hanoi | ? | ? | O(exp(n)) | ? | O(exp(n)) |
| costa/jvm-cost/Incr | O(n) | ? | O(n) | O(n) | O(n) |
| costa/jvm-cost/LinEqSolve | ? | ? | ? | O(n3) | O(n3) |
| costa/jvm-cost/ListInter | ? | ? | O(n2) | O(n2) | O(n2) |
| costa/jvm-cost/ListReverse | O(n) | ? | O(n) | O(n) | O(n) |
| costa/jvm-cost/MatMult | O(n3) | ? | O(exp(n)) | O(n3) | O(n3) |
| costa/jvm-cost/Matrixinverse | ? | ? | ? | O(n3) | O(n3) |
| costa/jvm-cost/MergeList | O(n) | ? | O(n) | O(n) | O(n) |
| costa/jvm-cost/Polynomial | O(1) | ? | O(1) | O(1) | O(1) |
| costa/jvm-cost/Power | O(n) | ? | O(n) | O(n) | O(n) |
| costa/jvm-cost/SelectOrd | O(1) | ? | O(n2) | O(n2) | O(n2) |
| costa/jvm-cost/ms | ? | ? | ? | ? | O(n2) |
| costa/misc/ack | ? | ? | ? | ? | ? |
| costa/misc/direct_n_log_n | O(log(n)) | O(n) | O(n) | O(n) | O(log(n)) |
| costa/misc/divide_and_conquer | O(n) | ? | O(n) | ? | O(exp(n)) |
| costa/misc/exponential | ? | ? | O(exp(n)) | ? | O(exp(n)) |
| costa/misc/linear | O(n) | O(n) | O(n) | O(n) | O(n) |
| costa/misc/logarithmic | O(1) | ? | O(1) | ? | ? |
| costa/misc/merge | O(n) | O(n) | O(n) | O(n) | O(n) |
| costa/misc/ms | O(n) | ? | O(n) | ? | O(n) |
| costa/misc/mspe | O(n) | O(n) | O(n) | O(n) | O(n) |
| costa/misc/n_log_n | O(1) | ? | O(1) | ? | ? |
| costa/misc/no_cover_point | ? | ? | O(exp(n)) | ? | ? |
| costa/misc/quadratic | O(n2) | ? | O(n2) | O(n2) | O(n2) |
| solved | 359 | 309 | 404 | 347 | 285 |
| minimal | 317 | 271 | 358 | 312 | 270 |
| constant | 119 | 118 | 131 | 117 | 109 |
| <= linear | 282 | 250 | 298 | 270 | 240 |
| <= quadratic | 346 | 300 | 376 | 336 | 270 |
| <= cubic | 356 | 306 | 383 | 345 | 278 |
| exponential | 0 | 0 | 18 | 0 | 7 |
| logarithmic | 2 | 0 | 0 | 0 | 4 |
The following list collects deterministic logic programs in LCTRS representation:
- dds_dds1.1.corr.its (output O(n)
- dds_dds1.1 (output O(n))
- various_pql (output ?
- various_sicstus1 (output O(n))
- www_split (output O(n))
- maxlength (output O(n))