{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:19:34Z","timestamp":1781075974674,"version":"3.54.1"},"reference-count":35,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/lics.2002.1029817","type":"proceedings-article","created":{"date-parts":[[2003,6,25]],"date-time":"2003-06-25T18:14:31Z","timestamp":1056564871000},"page":"55-74","source":"Crossref","is-referenced-by-count":775,"title":["Separation logic: a logic for shared mutable data structures"],"prefix":"10.1109","author":[{"given":"J.C.","family":"Reynolds","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"35","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1007\/3-540-45931-6_28","article-title":"A semantic basis for local reasoning","volume":"2303","author":"yang","year":"2002","journal-title":"Lecture Notes in Computer Science"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1145\/362452.362489"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3472-0_6"},{"key":"33","first-page":"41","article-title":"An example of local reasoning in BI pointer logic: The Schorr-Waite graph marking algorithm","author":"yang","year":"2001","journal-title":"SPACE 2001 Informal Proceedings of Workshop on Semantics Program Analysis and Computing Environments for Memory Management"},{"key":"15","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","author":"harel","year":"2000","journal-title":"Dynamic Logic"},{"key":"34","author":"yang","year":"2001","journal-title":"Local Reasoning for Stateful Programs"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45500-0_13"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45793-3_13"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325742"},{"key":"12","article-title":"The query language TQL","author":"conforti","year":"2002","journal-title":"Proc Workshop Web and Databases (WebDB)"},{"key":"21","author":"o'hearn","year":"2001","journal-title":"Notes on conditional critical regions in spatial pointer logic"},{"key":"20","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/BFb0055511","article-title":"Stack-based typed assembly language","volume":"1473","author":"morrisett","year":"1998","journal-title":"Lecture Notes in Computer Science"},{"key":"22","author":"o'hearn","year":"2002","journal-title":"Notes on separation logic for shared-variable concurrency"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","article-title":"Local reasoning about programs that alter data structures","volume":"2142","author":"o'hearn","year":"2001","journal-title":"Lecture Notes in Computer Science"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"26","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-0091-7","author":"pym","year":"2002","journal-title":"The Semantics and Proof Theory of the Logic of Bunched Implications"},{"key":"27","author":"reynolds","year":"1981","journal-title":"The Crafi of Programming"},{"key":"28","first-page":"303","article-title":"Intuitionistic reasoning about shared mutable data structure","author":"reynolds","year":"2000","journal-title":"Millennial Perspectives in Computer Science"},{"key":"29","author":"reynolds","year":"2000","journal-title":"Lectures on reasoning about shared mutable data structure"},{"key":"3","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/BFb0053562","article-title":"Verifiable and executable specifications of concurrent objects in L?","volume":"1381","author":"caires","year":"1998","journal-title":"Lecture Notes in Computer Science"},{"key":"2","first-page":"23","article-title":"Some techniques for proving correctness of programs which alter data structures","volume":"7","author":"burstall","year":"1972","journal-title":"Machine Intelligence"},{"key":"10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-45309-1_1","article-title":"A query language based on the ambient logic","volume":"2028","author":"cardelli","year":"2001","journal-title":"Lecture Notes in Computer Science"},{"key":"1","author":"bornat","year":"2001","journal-title":"Explicit description in BI pointer logic"},{"key":"30","first-page":"7","article-title":"Reasoning about shared mutable data structure (abstract of invited lecture)","author":"reynolds","year":"2001","journal-title":"SPACE 2001 Informal Proceedings of Workshop on Semantics Program Analysis and Computing Environments for Memory Management"},{"key":"7","author":"calcagno","year":"2001","journal-title":"Program logic and equivalence in the presence of garbage collection"},{"key":"6","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-45315-6_9","article-title":"On garbage and program logic","volume":"2030","author":"calcagno","year":"2001","journal-title":"Lecture Notes in Computer Science"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45332-6_7"},{"key":"5","author":"calcagno","year":"2002","journal-title":"Semantic and Logical Properties of Stateful Programmming"},{"key":"31","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1145\/174675.177855","article-title":"Implementation of the typed call-by-value ?-calculus using a stack of regions","author":"tofte","year":"1994","journal-title":"Conference Record of POPL '97 The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"},{"key":"4","first-page":"11","article-title":"Program logics in the presence of garbage collection (abstract)","author":"calcagno","year":"2001","journal-title":"SPACE 2001 Informal Proceedings of Workshop on Semantics Program Analysis and Computing Environments for Memory Management"},{"key":"9","article-title":"A spatial logic for querying graphs","author":"cardelli","year":"2002","journal-title":"Automata Languages and Programming"},{"key":"8","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/3-540-45294-X_10","article-title":"Computability and complexity results for a spatial assertion language for data structures","author":"calcagno","year":"2001","journal-title":"Lecture Notes in Computer Science"}],"event":{"name":"17th Annual IEEE Symposium on Logic in Computer Science","location":"Copenhagen, Denmark","acronym":"LICS-02"},"container-title":["Proceedings 17th Annual IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8005\/22127\/01029817.pdf?arnumber=1029817","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,23]],"date-time":"2020-03-23T20:33:12Z","timestamp":1584995592000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1029817\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":35,"URL":"https:\/\/doi.org\/10.1109\/lics.2002.1029817","relation":{},"subject":[]}}