🚀 AProVE is now open source!

For more than two decades, our group at RWTH Aachen University has been developing AProVE — one of the most powerful systems for fully automated termination, complexity, and safety proofs. As of now, its source code is publicly available under the LGPL. 🎉

AProVE automatically answers questions that are undecidable in general, yet it handles them remarkably well in practice: ✅ Does this program terminate on every input? ⏱️ How costly can its execution become in the worst case?

And it does so not only for term rewrite systems, but for many real-world languages and formalisms: 🔹 Java (bytecode) 🔹 C / LLVM 🔹 Haskell 🔹 Prolog 🔹 Integer transition systems 🔹 Probabilistic programs & probabilistic term rewriting

Along the way, AProVE has earned numerous first places at the annual International Termination Competition, strong results at SV-COMP, and two Kurt Gödel medals at the Vienna Summer of Logic 2014.

With this release, AProVE’s modular framework of processors, strategies, and backend solvers is open for everyone to study, use, and extend. Want to add support for a new language, plug in your own analysis technique, or integrate another solver? Contributions are very welcome!

🔗 Code: https://github.com/aprove-developers/aprove-open-source 🌐 Website: https://aprove.informatik.rwth-aachen.de

#OpenSource #FormalMethods #ProgramVerification #TerminationAnalysis #TermRewriting #RWTHAachen #ResearchSoftware