Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols

Explore an innovative approach to formally verifying infinite-state systems in this 16-minute conference talk from OOPSLA2 2023. Delve into a proposed interactive verification methodology that employs relational abstraction to mitigate solver divergence when dealing with quantifiers. Learn how this technique abstracts functions in verification conditions as one-to-one relations, avoiding function cycles and the proliferation of ground terms. Discover the benefits of this sound approach, including guaranteed correctness when solvers cannot find counter-models, and understand how to address false counterexamples through abstraction refinement. Examine the application of this method in Ivy for verifying safety properties of consensus protocols, and gain insights into its effectiveness in automatically verifying most goals, providing valuable guidance through counterexamples, and deriving efficient low-level implementations of complex algorithms.