Automated Datastructure Verification Using Unfoldings and SMT Solving - Foundations and FO-Completeness

Explore the foundations and applications of automated datastructure verification in this comprehensive tutorial from TutorialFest at POPL'24. Delve into the recent heuristic technique of unfolding recursive definitions combined with quantifier-free SMT reasoning for both functional and imperative programs. Examine the theoretical foundations that demonstrate the completeness of these heuristics for certain abstractions of the verification problem. Gain insights into the role of user assistance in tools employing these methods and discover new techniques for quantified first-order logic reasoning over combined theories using SMT solvers. Learn about the technique's completeness results and its practical applications in verifying programs that manipulate datastructures. Presented by P. Madhusudan and Adithya Murali, this 2-hour and 57-minute session offers a deep dive into the cutting-edge approaches in automated program verification.

[TutorialFest@POPL'24] Automated Datastructure Verification using Unfoldings and SMT Solvi...