Property-Agnostic Base Case Extension for Scalable Verification of Distributed Systems

This conference talk presents a novel method for proving temporal properties in distributed systems with ring topologies, allowing verification results from small systems to extend to arbitrarily large ones. Learn how researchers from Brigham Young University combine model checking with theorem proving to establish a conformance relation that ensures properties verified in base cases hold in larger systems. The approach is demonstrated through a case study of a nontrivial distributed protocol used in MyCHIP's digital currency for credit clearing. The presentation includes techniques for proving that adding new nodes to a ring topology doesn't affect the possible states of existing nodes, thereby maintaining verified temporal properties across system scaling. Attend this 25-minute talk at the VMCAI conference (January 20-21, 2025) to discover scalable verification techniques that overcome traditional model checking limitations.