Formally verifying exceptions for low-level code with separation logic

Marco Paviotti, Jesper Bengtson. Formally verifying exceptions for low-level code with separation logic. Journal of Logic and Algebraic Programming, 94:1-14, 2018. [doi]