"Proving pointer programs in higher-order logic."

Farhad Mehta, Tobias Nipkow (2005)
a service of Schloss Dagstuhl - Leibniz Center for Informatics