Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
This conference talk from POPL 2025 presents research on bridging the semantic gap in first-order logic when used for abstract modeling of complex systems. Learn how researchers Neta Elad and Sharon Shoham from Tel Aviv University tackle the problem of spurious states that arise from first-order logic abstractions. The presentation introduces an approach for refining first-order abstractions using induction axioms for abstract order relations, formalizing sound axiom schemata for well-founded and finite-domain semantics. Discover how spurious counter-models can guide the instantiation of these axiom schemata, and explore their sound and complete reduction to standard semantics in the Ordered Self-Cycle fragment of first-order logic. The researchers demonstrate their prototype tool's effectiveness in eliminating spurious system states that block verification progress in distributed protocols and heap-manipulating programs. This 20-minute talk includes reusable artifacts available through Zenodo for further exploration of the techniques presented.
