If you are interested in this sort of thing you can also have a look at HIP/SLEEK Verification System - http://loris-7.ddns.comp.nus.edu.sg/~project/TeachHIP/

It uses separation logic which is an extension of Hoare logic for programs that manipulate the heap.