Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
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.
