Separation Logic for Multithreaded Object-Oriented Languages by Clément Hurlin