HFL(Z) Validity Checking for Automated Program Verification

on YouTube ↗22m

" summary

Proposes an automated validity checker for HFL(Z) formulas that encodes higher-order program verification (termination, nontermination, fair variants, branching-time) into logic validity. Least fixed points are under-approximated by bounded unfoldings using parameters of the form c·x+d, then converted to greatest-fixed-only formulas and fed to existing greatest-fixed validity tools. Implements the pipeline and reports it outperforms four prior specialized verifiers on the POPL benchmark suite; method is sound and incomplete.

AI-written summary · about

" chapters (12)

1. 0:00HFL(Z) validity checking intro
2. 1:25What is HFL(Z) and why
3. 2:29HFL(Z) syntax and semantics
4. 4:18HFL(Z) for program verification
5. 7:14Method overview
6. 9:43Approximating least fixed points
7. 12:37Higher-order predicates in approx
8. 15:47Power and limits of method
9. 17:09Experimental results
10. 18:33Conclusion and future
11. 19:15Q&A: Comparison with others
12. 19:58Q&A: Bounds for unfolding