Google, IBM & Meta Certificates — All 10,000+ Courses at 40% Off
One annual plan covers every course and certificate on Coursera. 40% off for a limited time.
Get Full Access
Watch this 21-minute conference talk from POPL 2025 where researchers Patrick Cousot and Jeffery Wang from New York University present their work on designing logics for proving hyperproperties of iterative programs using abstract interpretation principles. The presentation is structured in three parts: first introducing a generic, structural, fixpoint abstract interpreter parameterized by an algebraic abstract domain for various program semantics; second, defining exact and approximate semantic abstractions that preserve mathematical structures; and third, exploring abstractions of semantic properties that yield simplified proof rules, including algebraic generalizations of hyperlogics. Learn about advanced concepts in program verification including abstract interpretation, calculational design, hyperlogics, hyperproperties, and various forms of semantic abstractions. The talk is based on their paper published in ACM SIGPLAN, with supplementary materials available online.
