Approximations for Analyzing Infinite-State Systems

Abstract

Computer software is one of the most critical parts of modern society. Hence, ensuring its correctness through rigorous modelling and verification is essential. Infinite-state systems are an important paradigm for modelling software. However, for many such systems, even fundamental problems like safety verification are undecidable or computationally intractable. This necessitates the study of efficient over-approximations for analysing such systems. An over-approximation of a system is another system that contains all of the behaviours of the original system (and possibly more). Thus, proving safety in the over-approximation ensures safety in the original system as well.

In this talk, I will present some results on efficiently over-approximating infinite-state systems, by moving from discrete domains to continuous domains. On the theoretical side, we will show that this continuous over-approximation results in a much better decidability and complexity landscape for various well-studied classes of infinite-state systems. On the practical side, we will show how these techniques can be used to verify fault-tolerant distributed algorithms and report experimental results on a set of benchmarks from the literature.

About the Speaker

Dr Balasubramanian A Ramachandrakumar is a postdoctoral researcher at the Max Planck Institute for Software Systems (MPI SWS), Germany. He received his PhD from the Technical University of Munich under Prof Javier Esparza and served there as interim professor between Oct 2024 and Mar 2025.

His research lies at the intersection of theory and formal methods, where he has developed techniques for the efficient algorithmic analysis of infinite-state systems. He has published 23 papers, including at LICS, POPL, PLDI and CONCUR and is the recipient of a Distinguished Paper Award at LICS 2025 and the Best Paper Award at CONCUR 2026.