{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T21:15:46Z","timestamp":1775769346081,"version":"3.50.1"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2015,2,27]],"date-time":"2015-02-27T00:00:00Z","timestamp":1424995200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["258405"],"award-info":[{"award-number":["258405"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>This paper presents a program logic for reasoning about multithreaded\nJava-like programs with dynamic thread creation, thread joining and reentrant\nobject monitors. The logic is based on concurrent separation logic. It is the\nfirst detailed adaptation of concurrent separation logic to a multithreaded\nJava-like language. The program logic associates a unique static access\npermission with each heap location, ensuring exclusive write accesses and\nruling out data races. Concurrent reads are supported through fractional\npermissions. Permissions can be transferred between threads upon thread\nstarting, thread joining, initial monitor entrancies and final monitor exits.\nIn order to distinguish between initial monitor entrancies and monitor\nreentrancies, auxiliary variables keep track of multisets of currently held\nmonitors. Data abstraction and behavioral subtyping are facilitated through\nabstract predicates, which are also used to represent monitor invariants,\npreconditions for thread starting and postconditions for thread joining.\nValue-parametrized types allow to conveniently capture common strong global\ninvariants, like static object ownership relations. The program logic is\npresented for a model language with Java-like classes and interfaces, the\nsoundness of the program logic is proven, and a number of illustrative examples\nare presented.<\/jats:p>","DOI":"10.2168\/lmcs-11(1:2)2015","type":"journal-article","created":{"date-parts":[[2015,5,18]],"date-time":"2015-05-18T07:33:27Z","timestamp":1431934407000},"source":"Crossref","is-referenced-by-count":26,"title":["Permission-Based Separation Logic for Multithreaded Java Programs"],"prefix":"10.46298","volume":"Volume 11, Issue 1","author":[{"given":"Christian","family":"Haack","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4467-072X","authenticated-orcid":false,"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]},{"given":"Cl\u00e9ment","family":"Hurlin","sequence":"additional","affiliation":[]},{"given":"Afshin","family":"Amighi","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2015,2,27]]},"reference":[{"key":"793:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/998\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/998\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:00:52Z","timestamp":1681243252000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/998"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,27]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-11(1:2)2015","relation":{"is-same-as":[{"id-type":"arxiv","id":"1411.0851","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1411.0851","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1007\/978-3-319-66845-1_7","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,2,27]]},"article-number":"998"}}