While programs

Fact. Every while program can be simulated by a while program with at most one while loop.

Harel's proof using structural induction
Kozen's proof using KAT
Kleene Algebra with Tests (KAT)
Kozen's lecture notes on KAT
Kozen's result about the complexity & decidability of KAT

Talks on program verification

Selected Topics in Design & Verification
Vardi's fun lectures on automated verification and synthesis
Fast Interpolating Bounded Model Checking