Automated reasoning about program termination and complexity
Releases · Developer Guide · Issues · Intro Video
Current release: 1.0.0 Capybara
AProVE is an automated verification framework for proving properties such as termination and worst-case complexity. It is developed by the Programming Languages and Verification group at RWTH Aachen University.
At a high level, AProVE helps answer questions like:
- Does this program terminate on all inputs?
- How time consuming can its execution become in the worst case?
- Can these properties be derived automatically from a formal model of the program?
AProVE supports several programming paradigms and input languages, including rewriting-based, imperative, functional, and logic-oriented formalisms. Instead of relying on testing alone, it builds machine-checkable proof obligations and solves them with formal methods.
| Capability | Description |
|---|---|
| Termination analysis | Proves whether a program always terminates |
| Complexity analysis | Derives lower and upper bounds on runtime |
| Multiple formalisms | Supports languages such as Java, C, Haskell, and Prolog |
| Extensible architecture | New processors, strategies, and backends can be integrated |
AProVE follows a transform-and-analyze approach:
- Translate the input program into an internal problem representation.
- Apply processors that simplify, decompose, or solve the problem.
- Use strategies to orchestrate the analysis flow.
- Delegate specialized proof obligations to backend solvers.
- Combine all intermediate results into a final result.
Typical outcomes include YES, NO, and MAYBE for termination, as well as complexity bounds such as O(1), O(n), or EXP.
The core system is organized around four concepts.
A problem captures the current analysis state. For example, a term rewrite system may be represented as a TRSProblem.
Processors are the main transformation units in AProVE. They either simplify a problem, split it into subproblems, or solve it directly.
Strategies control which processors are applied, in which order, and under which conditions.
Solvers handle specific mathematical subproblems. AProVE integrates backend technologies such as SAT and SMT solvers, as well as domain-specific tools like KoAT for complexity analysis.
For local development and build instructions, see the project wiki:
https://github.com/aprove-developers/aprove-open-source/wiki
Contributions are welcome. AProVE is particularly well suited for extending:
- supported input languages and problem representations
- analysis processors and strategies
- solver integrations and backend tooling
If you plan to contribute code, start with the wiki and the existing architecture sections above so you can place new work into the right abstraction layer.
- Releases: GitHub Releases
- Issues: Bug reports and feature requests
- Discussions: Community discussions
- Code of Conduct: CODE_OF_CONDUCT.md
- Contributing Guide: CONTRIBUTING.md