-
Notifications
You must be signed in to change notification settings - Fork 0
List of tools
carlaferreira edited this page Sep 22, 2025
·
28 revisions
The following table contains all tools that are known to the EuroProofNet Program Verification inventory. It contains:
- tools competing in SV-COMP
- tools competing in Termination competition
- tools analyzing the termination and complexity bounds (as a special case of termination)
- TBU
Please click on the prover name for its detailed profile (if available) or contribute with yours.
| Name | Website | Used for | Input formats | Status |
|---|---|---|---|---|
| Alk Platform | link | analyzing and understanding algorithms' behavior | Alk, a simple algorithmic language | maintained |
| AProVE | link | proving (non-)termination, finding upper/lower complexity bounds | C, Haskell, Java Bytecode, Prolog, TRS | maintained |
| Bubaak | link | proving assertions safety, memory safety, defined behavior, (non-)termination | C, LLVM | maintained |
| KeY | link | functional verification, proving termination, proving relational properties | Java, Java Modeling Language (JML) for specification | maintained |
| KoAT | link | proving termination, finding upper complexity bounds | (Probabilistic) ITS, C Integer | maintained |
| NTI | link | proving (non-)termination | TRS, Logic Programming | maintained |
| Rapid | link | invariant generation, proving partial correctness | While | maintained |
| TriCera | link | invariant generation, proving partial correctness, contract inference | C | maintained |
| TTT2 | link | proving (non-)termination | TRS | maintained |
| Stainless | link | functional verification, proving termination | Scala | maintained |
| IsaVODEs | Part of Isabelle/UTP | partial correctness, termination and reachability of cyber-physical systems | Isabelle/HOL's hybrid programs | maintained |
| Mopsa | webpage gitlab | Sound, automated platform for static analysis. Checks for runtime errors. | C and Python programs | maintained |
| MuVal | link | proving (non-)termination and temporal properties | C Integer, ITS, ... | maintained |
| My tool | link | proving termination, invariant generation | C | maintained |
| VeriFast | link | functional verification, proving termination | C, Java, C++ (preview), Rust (under development) with VeriFast annotation syntax | maintained |
| Wanda | link | proving (non-)termination of higher-order term rewriting systems | Plain HO-TRS | somewhat maintained |
| CeTA | link | certification of untrusted proofs on (non)termination, (non)confluence, safety | CPF, mostly for TRS | maintained |
| crest | link | analysis of logically constrained term rewrite systems (mostly (non-)confluence and (non-)termination) | LCTRS | maintained |
| link | proving partial correctness | C | not maintained | |
| ESBMC | link | Context-bounded model checker for verifying single and multithreaded programs | C/C++, CUDA, CHERI, Kotlin, Python, and Solidity | maintained |
| LoAT | link | (dis)proving satisfiability of Constrained Horn Clauses, disproving termination, finding lower complexity bounds | CHCs, Transition Systems in SMT-LIB, KoAT's native input format | maintained |
| JaTyC | link | typestate verification | Java, Typestate specifications | maintained |
| Cameleer | link | Functional verification, termination | OCaml, GOSPEL specifications | maintained |
| VeriFx | link | Fully automated verification of high-level correctness properties | Specialised functional OOP language, inspired by Scala | maintained |