Finding Infinite Counter-Models in Deductive Verification

Explore a groundbreaking approach to finding infinite counter-models in deductive verification presented at POPL 2024. Delve into the challenges of quantified formulas in first-order logic and their impact on automated solvers. Learn about a novel method that introduces symbolic structures to represent infinite models, an effective model finding procedure, and a new decidable fragment of first-order logic. Discover how this approach quickly identifies infinite counter-models for verification failures in distributed consensus protocols and heap-manipulating programs, outperforming state-of-the-art SMT solvers and theorem provers. Gain insights into improving deductive verification processes and understanding verification failures through this 19-minute video presentation by researchers from Tel Aviv University and VMware Research.