Reducing Liveness to Safety in First-Order Logic

Watch a 26-minute conference presentation from POPL 2018 that introduces a novel technique for verifying temporal properties of infinite-state distributed systems. Learn how to reduce temporal verification problems to safety verification in first-order logic, enabling verification of previously unverified distributed protocols. Explore how this approach models infinite-state systems and uses first-order temporal logic (FO-LTL) to handle both unbounded parallelism and infinite-state per process. Understand the innovative fair cycle detection method that overcomes the challenges of infinitely many states and fairness constraints, offering an alternative to traditional well-founded relations. See practical applications demonstrated through mechanized liveness proofs for protocols like TLB Shootdown and Stoppable Paxos, with special attention to verification using effectively propositional first-order logic (EPR).