Permission-Based Separation Logic for Multithreaded Java Programs (Logical Methods in Computer Science, 2015)