October 21, 2022
Due to their ubiquity, distributed systems are an important target for formal verification. However, these systems present challenges for formal verification when their behavior is parameterized (i.e., the number of processes in the system in unknown or unbounded). One possible solution for overcoming these challenges is to leverage cutoff results, a type of Turing reduction which allows us to verify the system with an arbitrary number of processes by model checking the system with a concrete, finite number of processes. Existing cutoff reductions often rely on control flow independence of processes and cannot be applied when these processes’ behavior is heavily intertwined, such as in client-server applications. The prevalence of client-server architectures in practical applications make them an appealing target for the development of novel cutoff reduction techniques. In this talk, I will discuss how we can exploit properties of a class of parameterized client-server applications to derive efficient process cutoffs and enable fully-automated safety verification for these parameterized systems.
About Chris Wagner
Chris Wagner is a fifth-year Computer Science PhD student at Purdue University working with Prof. Roopsha Samanta at the intersection of distributed systems and programming languages. His research focuses on automated reductions for formal verification of parameterized systems.