Brief Announcement: Automating and Mechanising Cutoff Proofs for Parameterized Verification of Distributed Protocols


We propose a framework to automate and mechanize simulation-based proofs of cutoffs for parameterized verification of distributed protocols. We propose a strategy to derive the simulation relation given the cutoff instance and encode the correctness of the simulation relation as a formula in first-order logic. We have successfully applied our approach on a number of distributed protocols.

International Symposium on Distributed Computing