Calculational Design of Hyperlogics by Abstract Interpretation

on YouTube ↗21m

" summary

Claims a calculational pipeline that starts from an algebraic semantics and builds a structural fixpoint abstract interpreter parameterized by algebraic abstract domains to yield concrete Post and hyper-Post transformers, then derives sound-and-complete hyperlogics (so completeness holds but the fully precise logic is unmanageable). Defines exact and approximate semantic abstractions that preserve collecting and hypercollecting structure, and introduces concrete algebraic abstractions — including join/homomorphic/principal-ideal and chain limit algebraic abstraction — that recover usable forall/exists-style hyperlogics.

AI-written summary · about

" chapters (15)

1. 0:00Introduction
2. 1:07Calculating hyperlogics
3. 2:10Algebraic semantics
4. 3:35Induction in semantics
5. 5:03Program properties encoding
6. 6:27Hyperproperties transformers
7. 7:30Logic structural challenges
8. 8:58Soundness and completeness
9. 10:07Abstraction propagation
10. 10:50For-exist abstraction
11. 12:36Fixpoint iteration issues
12. 13:44Logic for traces
13. 14:06Conclusion on logic
14. 15:30Summary and inverse logic
15. 17:14Q&A