//

Press N to jot a timestamped note or B to pin a moment while watching.
A method for verifying compiler loop optimizations by integrating small-step and big-step semantics, introducing an abstract behavioral semantics for a unified framework.
Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations (Video, LOPSTR+PPDP 2026) David Knothe, and Oliver Bringmann (FZI Research Center for Information Technology; FZI Research Center for Information Technology)