{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T22:00:54Z","timestamp":1693864854952},"reference-count":23,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3619,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1016\/s1571-0661(05)82560-5","type":"journal-article","created":{"date-parts":[[2005,5,20]],"date-time":"2005-05-20T09:21:17Z","timestamp":1116580877000},"page":"518-539","source":"Crossref","is-referenced-by-count":22,"title":["Transactions for Software Model Checking"],"prefix":"10.1016","volume":"89","author":[{"given":"Cormac","family":"Flanagan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)82560-5_BIBBLR02","series-title":"OOPSLA 02: Object-Oriented Programming, Systems, Languages, and Applications","first-page":"211","article-title":"Ownership types for safe programming: preventing data races and deadlocks","author":"Boyapati","year":"2002"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBBR01","series-title":"OOPSLA 01: Object-Oriented Programming, Systems, Languages, and Applications","first-page":"56","article-title":"A parameterized type system for race-free Java programs","author":"Boyapati","year":"2001"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBCL98","series-title":"CONCUR 98: Concurrency Theory, volume 1466 of Lecture Notes in Computer Science","first-page":"317","article-title":"Reduction in TLA","author":"Cohen","year":"1998"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBDHRR03","article-title":"Exploiting object escape and locking information in partial order reductions for concurrent object-oriented programs","author":"Dwyer","year":"2003","journal-title":"Technical Report SAnToSTR2003-1, Department of Computing and Information Sciences, Kansas State University"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBDOE77","series-title":"Parallel program correctness through refinement POPL 77: Principles of Programming Languages","first-page":"155","author":"Doeppner","year":"1977"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBFF00","series-title":"PLDI 00: Programming Language Design and Implementation","first-page":"219","article-title":"Type-based race detection for Java","author":"Flanagan","year":"2000"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBFQ02","article-title":"Checking concise specifications for multithreaded software","author":"Freund","year":"2002","journal-title":"Technical Note 01-2002, Williams College"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBFQ03A","series-title":"SPIN 03: Workshop on Model Checking Software, volume 2648 of Lecture Notes in Computer Science","first-page":"213","article-title":"Thread-modular model checking","author":"Flanagan","year":"2003"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBFQ03B","series-title":"PLDI 03: Programming Language Design and Implementation to appear","article-title":"A type and effect system for atomicity","author":"Flanagan","year":"2003"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBFQ03C","series-title":"TLDI 03: Types in Language Design and Implementation","first-page":"1","article-title":"Types for atomicity","author":"Flanagan","year":"2003"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBGOD96","series-title":"Lecture Notes in Computer Science 1032","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","article-title":"Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem","author":"Godefroid","year":"1996"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBGRO03","series-title":"TLDI 03: Types in Language Design and Implementation","first-page":"13","article-title":"Type-safe multithreading in Cyclone","author":"Grossman","year":"2003"},{"issue":"3","key":"10.1016\/S1571-0661(05)82560-5_BIBHW90","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/78969.78972","article-title":"Linearizability: A correctness condition for concurrent objects","volume":"12","author":"Herlihy","year":"1990","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBLAM94","article-title":"How to write a long formula","author":"Lamport","year":"1994","journal-title":"Technical Report 119, DEC Systems Research Center"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBLIP75","first-page":"717","article-title":"Reduction: A method of proving properties of parallel programs","volume":"18:12","author":"Lipton","year":"1975"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBLS89","article-title":"Pretending atomicity","author":"Lamport","year":"1989","journal-title":"Research Report 44, DEC Systems Research Center"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBMIS01","series-title":"A Discipline of Multiprogramming: Programming Theory for Distributed Applications","author":"Misra","year":"2001"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBPAP86","series-title":"The theory of database concurrency control","author":"Papadimitriou","year":"1986"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBPEL94","first-page":"377","article-title":"Combining partial order reductions with on-the-fly model checking","volume":"818","author":"Peled","year":"1994"},{"issue":"4","key":"10.1016\/S1571-0661(05)82560-5_SBN97","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1145\/265924.265927","article-title":"Eraser: A dynamic data race detector for multithreaded programs","volume":"15","author":"Savage","year":"1997","journal-title":"ACM Transactions on Computer Systems"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBSC03","series-title":"TACAS 03: Tools and Algorithms for the Construction and Analysis of Systems, volume 2619 of Lecture Notes in Computer Science","first-page":"489","article-title":"Optimistic synchronization-based state-space reduction","author":"Stoller","year":"2003"},{"issue":"2","key":"10.1016\/S1571-0661(05)82560-5_BIBTAR72","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","article-title":"Depth first search and linear graph algorithms","volume":"1","author":"Tarjan","year":"1972","journal-title":"SIAM Journal of Computing"},{"key":"10.1016\/S1571-0661(05)82560-5_BIBVAL90","first-page":"25","article-title":"A stubborn attack on state explosion","volume":"531","author":"Valmari","year":"1990"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105825605?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105825605?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,26]],"date-time":"2019-01-26T05:50:25Z","timestamp":1548481825000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105825605"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S1571066105825605"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)82560-5","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}