On the Power of Temporal Prophecy

Explore a 35-minute video presentation by Jochen Hoenicke from Certora at the PODELSKI workshop, focusing on the power of temporal prophecy in liveness and termination proofs. Delve into a technique that reduces temporal proofs to verification conditions in uninterpreted first-order logic using fair abstract lassos. Discover how temporal prophecy enhances this method, enabling it to prove termination of nested loops and even the non-primitive recursive Ackermann function. Gain insights into the technique's ability to handle "infinitely-many" nested loops, demonstrating its significant power in program verification. Presented at the ACM SIGPLAN-sponsored PODELSKI workshop on June 25, 2024, this talk offers valuable knowledge for researchers and practitioners in program verification and formal methods.