Using Property-Driven Reductions to Verify Distributed Systems Automatically

Distributed systems form an integral part of modern infrastructure. Due to their ubiquity, even a small design error can cause widespread harm. With their immense state spaces and complex behaviors, which can conceal bugs until very specific circumstances arise, distributed systems are popular targets for formal verification. However, many common properties of realistic distributed systems, such as large variable domains and arbitrary numbers of interacting processes, make them challenging verification targets. In this talk, I will present an approach for automating parameterized verification via cutoff reductions, focusing on our most recent results targeting parameterized client-server systems.

About Chris Wagner

Chris Wagner is a PhD candidate in his 7th year at Purdue working with Prof. Ben Delaware and Roopsha Samanta. His research focuses on programming languages, distributed systems, and formal verification.