thesis-evaluation

Tools used for the evaluation

• AProVE
• APRON (dependency of KoAT)
• CoFloCo (statically linked)
• KoAT
• LoAT (statically linked)
• MiniSmt (dependency of TCT)
• TCT
• Z3 (dependency of AProVE, KoAT, and TCT)

AProVE strategies used for the evaluation

• CDT
• constant bounds
  • standalone
  • with strategy switching
• detect extra variables on right-hand sides
• induction technique
  • standalone
  • with argument filtering
  • with indefinite lemmas
  • with argument filtering and indefinite lemmas
  • with argument filtering, indefinite lemmas, and strategy switching
• loop detection
  • standalone
  • with argument filtering
  • with strategy switching
• JBC
  • lower bounds without SMT encoding
  • lower bounds with SMT encoding
  • upper bounds
• Matchbounds
• TCT
  • preprocessing
  • preprocessing and strategy switching
• TRS via CoFloCo
• TRS via RNTS

Details

• AProVE
  • flags that were used for all benchmarks
    • -s $STRATEGY
    • -m benchmark
    • -t $TIMEOUT
  • flag to infer upper bounds for JBC: -O java::analysis_goal=time_complexity
  • flags to infer lower bounds for JBC: -O java::analysis_goal=time_complexity -O java::show_lower_bounds=true
• analyzing TRSs with CoFloCo
  • additional option as RNTS-backend: -compute_lbs no
  • additional options as standalone-backend: -compute_lbs no -compress_chains 2 -solve_fast
• LoAT
  • flag to enable SMT encoding of limit problems: --limit-smt
• KoAT was invoked with -smt-solver z3-internal
• TCT
  • script to couple AProVE’s preprocessings with TCT