AProVE Update: New Version Available

We are pleased to announce the termination competition version of AProVE for the year 2026, featuring, e.g., novel techniques for the analysis of probabilistic term rewrite systems and some bugfixes in the analysis of C programs.

What’s New?

Updates on the Analysis of PTRSs

AProVE also analyzes probabilistic term rewrite systems (PTRSs), where the goal is to prove or disprove almost-sure termination (AST), i.e., termination with probability 1, and strong almost-sure termination (SAST), i.e., expected bounded worst-case complexity.

• Decision procedure for AST: AProVE can now fully decide (i.e., always prove or disprove) almost-sure termination for specific subclasses of PTRSs. The theoretical results for this are presented at the VeriProb Workshop 2026.
• Loop finder for lower bounds on expected complexity, extending the technique from our upcoming IJCAR 2026 paper.
• Improved proof output when disproving (S)AST of PTRSs, extending our upcoming IJCAR 2026 paper.

Updates on the Strategy

New TermComp26 strategy, tuned for better speed across the competition categories.

Further Bugfixes

• Bit-vector arithmetic fixes: correct global-variable initial values, and signed-integer handling in the bit-vector setting.

The update of the Docker container on DockerHub will shortly follow. To get notified on news like this one, become a member of our mailing list! For this, please send an email with “subscribe” in the subject line to aprove-news-join@lists.rwth-aachen.de .

— The AProVE Team