December 10, 2021
Distributed systems underpin our daily lives so extensively that we often forget their presence. Due to their ubiquity, distributed systems are an important target for formal verification. However, many common properties of realistic distributed systems, such as unbounded variable domains and arbitrary numbers of interacting processes, make them challenging targets for verification. Recent results have shown that automatic verification of systems parameterized by the number of processes can be achieved when processes have a small, finite state space. Unfortunately, this technique is not sufficient for systems composed of processes with large or unbounded variable domains. In this talk, I will review recent parameterized verification and cutoff results, and present a novel reduction technique for reducing parameterized verification of a system with unbounded variable domains to that of one with small, bounded domains.