AProVE's Web Interface
This is the AProVE Web Interface for the current version of AProVE.
Pick the language of your input below. On the next page you can paste your program, upload a file, or load a preset example, and then let AProVE run on our servers. No installation is required. If you would rather run AProVE on your own machine, see the Get AProVE page.
Frontend Languages
Languages that programs are actually written in. AProVE translates them into rewrite systems internally.
Java Bytecode
Termination of Java programs given as source of a single class or as a jar file.
Java Bytecode Complexity
Upper bounds on the runtime complexity of Java programs.
C
Termination and memory safety of C programs, compiled to LLVM internally.
Functional Program (AProVE)
Termination of first-order functional programs in a simple ML-like syntax.
Prolog
Termination of logic programs written in Prolog.
LLVM
Termination and memory safety of programs given as LLVM intermediate representation.
Haskell
Termination of Haskell 98 programs.
Backend Languages
Analysis-oriented formalisms such as term rewrite systems and integer transition systems, which can also be given directly as input.
Term Rewrite System (WST Format)
Termination and complexity of TRSs in the old Termination Competition format.
Term Rewrite System (AProVE Format)
Termination and complexity of TRSs in AProVE's own human-readable format.
Probabilistic Term Rewrite System
Almost-sure termination and expected complexity of probabilistic TRSs.
(Probabilistic) Term Rewrite System (ARI Format)
Termination and complexity of (probabilistic) TRSs in the current ARI competition format.
String Rewrite System (WST Format)
Termination and complexity of SRSs in the old Termination Competition format.
String Rewrite System (AProVE Format)
Termination and complexity of SRSs in AProVE's own human-readable format.
Integer Term Rewrite System (RTA'09)
Termination of TRSs with built-in integers and integer constraints.
Integer Term Rewrite System (top-level rewriting)
Termination and complexity of integer transition systems written as rewrite rules.
Details on every input format, including syntax help pages, are collected on the Usage page.