\input zb-basic
\input zb-ioport
\iteman{io-port 70059634}
\itemau{Chlipala, Adam}
\itemti{Mostly-automated verification of low-level programs in computational separation logic}
\itemso{PLDI, 234-245 (2011).}
\itemcc{}
\itemut{}
\itemli{doi:10.1145/1993498.1993526}
\end