A unified memory model for pointers
LPAR, pp. 474-488, 2005.
One of the challenges in verifying systems level code is the low-level, untyped view of the machine state that operating systems have. We describe a way to faithfully formalise this view while at the same time providing an easy-to-use, abstract and typed view of memory where possible. We have used this formal memory model to verify parts ...More
Get fulltext within 24h
Full Text (Upload PDF)
PPT (Upload PPT)