"Formally verifying Exceptions for Low-level code with Separation Logic (Other)"^^ . . . . . . .