\input zb-basic
\input zb-ioport
\iteman{io-port 70647983}
\itemau{Mccreight, Andrew}
\itemti{Practical tactics for separation logic}
\itemso{TPHOLs, 343-358 (2009).}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-03359-9\_24}
\end