Skip to content

Stronger version of adequacy that also talks about state.

Robbert Krebbers requested to merge robbert/strong_adequacy into master

The predicate in adequacy is currently only able to talk about the return value of the main thread. After this change, it is also able to talk about the final state.

We make use of this in https://iris-project.org/pdfs/2018-iron.pdf (which is build on top of normal Iris weakest preconditions) to ensure via adequacy that all memory has been freed.

Edited by Robbert Krebbers

Merge request reports