PV1 ⊧ TcT: Tyrolean Complexity Tooldetermines the complexity, including proof, of a given integer transition system or term rewrite system

Application domain/field

• Complexity analysis
• Term rewrite systems
• Integer transition system
• Amortized resource analysis

Type of tool

Complexity analyser

Expected input

Program/system

Format:

Depends on the instance that is used:

• tct-its expects a .its file (integer transition system)
• tct-trs expects a .trs file (term rewrite system)
• tct-hoca expects a .fp file. It translates a pure fragment of OCaml to a TRS.
• tct-jbc expects a .trs file.

Expected output

If successful, textual representation of the obtained complexity judgement, and corresponding proof tree. If not successful, it will print the uncompleted proof tree and the reason for failure.

Internals

$T_{C}T$ has several instances which provide automated complexity analysis for different kinds of systems:

• tct-its for integer transition systems. Uses Yices.
• tct-trs for term rewrite systems. Uses MiniSmt
• tct-hoca for higher-order systems
• tct-jbc for Jinja bytecode. Uses Yices, MiniSmt

Comments

Also spellt as $T_{C}T$. License: BSD3