🇵🇹 Back home from FLoC 2026 in Lisbon!

I had the pleasure of attending this year’s Federated Logic Conference (FLoC) and presenting our paper “Disproving (Positive) Almost-Sure Termination of Probabilistic Term Rewriting via Random Walks” at IJCAR 2026 (joint work with Henri Nagel, Alexander Schlecht, and Jürgen Giesl).

In recent years, numerous techniques were developed to automatically prove termination of probabilistic programs. However, there are only a few automated methods to disprove their termination. In our paper, we present the first techniques to automatically disprove (positive) almost-sure termination of probabilistic term rewrite systems:

• Disproving termination of non-probabilistic systems requires finding a finite representation of an infinite computation, e.g., a loop of the rewrite system.

• In the probabilistic setting, a quantitative analysis is required: in addition to the existence of a loop, we have to count the number of such loops in order to embed suitable random walks into a computation.

• All our techniques are implemented in our fully automated tool AProVE, which has a simple web interface to test it out.

Beyond the talk, FLoC was a great time in general! Lots of interesting presentations and discussions with the termination, rewriting, probabilistic verification, and automated reasoning communities. I even got to work in the National Library of Portugal right next door.

If you are interested in this line of work, feel free to contact me!

📄 Paper: https://doi.org/10.1007/978-3-032-32592-1_18

🔗 arXiv: https://arxiv.org/abs/2602.16522

🌐 AProVE Website: https://aprove.informatik.rwth-aachen.de/

#FLoC2026 #IJCAR #Termination #TermRewriting #ProbabilisticPrograms #AutomatedReasoning