![]() |
|||||||
|
Automated Program Verification Environment
AProVE is a system for automated termination and complexity
proofs of
term rewrite systems (TRSs) and several variations of TRSs. Moreover, AProVE also handles several other formalisms, e.g.,
imperative programs (Java Bytecode and C / LLVM), functional programs (Haskell 98), and logic programs (Prolog).
The power of AProVE is demonstrated in the annual International Competition of Termination Tools and International Competition on Software Verification. AProVE also won two Kurt Gödel medals at VSL 2014 (report in German).
There are two possibilities to use AProVE:
|
||||||
Disclaimer |