University of Texas at Austin: Thomas Dillig's "Operational Semantics of an Imperative Language with Pointers"
Read these slides.
Click http://web.archive.org/web/20160727135935/http://www.cs.utexas.edu/~tdillig/cs345H/lecture16-6up.pdf link to open resource.