Verification of IBM 4765's Persistent Memory Manager

Here you can find the DownloadIsabelle theories (GZ, 258 KB) of our effort on verifying the Persistent Memory Manager used in IBM 4765. This work has been described in our FM 2014 paper.

To run the theories, you will need external pageIsabelle 2013. The theories have not been tested under the latest Isabelle release (2013-2 at the time of writing) and will probably not work with it out of the box.

To browse around, look at the provided README. Note that the theories are in a rough shape, albeit complete. To proof check the requirement compliance, you can run a batch build of the theories using:

isabelle build -d . -b Req

from the pmm subdirectory. Building the theories requires about an hour on an i5-powered laptop and consumes around 3GB of memory.

Authors

Ognjen Maric,