{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:55:49Z","timestamp":1725562549435},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642150562"},{"type":"electronic","value":"9783642150579"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15057-9_2","type":"book-chapter","created":{"date-parts":[[2010,8,11]],"date-time":"2010-08-11T07:01:15Z","timestamp":1281510075000},"page":"25-39","source":"Crossref","is-referenced-by-count":4,"title":["Tressa: Claiming the Future"],"prefix":"10.1007","author":[{"given":"Ali","family":"Sezgin","sequence":"first","affiliation":[]},{"given":"Serdar","family":"Tasiran","sequence":"additional","affiliation":[]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","first-page":"2","volume-title":"POPL 2009","author":"T. Elmas","year":"2009","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: POPL 2009, pp. 2\u201315. ACM, New York (2009)"},{"issue":"12","key":"2_CR2","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"R.J. Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM\u00a018(12), 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Larus, J.R., Rajwar, R.: Transactional Memory. Morgan & Claypool (2006)","DOI":"10.2200\/S00070ED1V01Y200611CAC002"},{"issue":"1","key":"2_CR4","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1016\/S0022-0000(75)80018-3","volume":"10","author":"E.A. Ashcroft","year":"1975","unstructured":"Ashcroft, E.A.: Proving assertions about parallel programs. J. Comput. Syst. Sci.\u00a010(1), 110\u2013135 (1975)","journal-title":"J. Comput. Syst. Sci."},{"issue":"5","key":"2_CR5","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S. Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM\u00a019(5), 279\u2013285 (1976)","journal-title":"Commun. ACM"},{"key":"2_CR6","volume-title":"PPoPP 2005","author":"L. Wang","year":"2005","unstructured":"Wang, L., Stoller, S.D.: Static analysis for programs with non-blocking synchronization. In: PPoPP 2005. ACM Press, New York (2005)"},{"issue":"1-3","key":"2_CR7","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P.W. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci.\u00a0375(1-3), 271\u2013307 (2007)","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"2_CR8","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1145\/780822.781169","volume":"38","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. SIGPLAN Not.\u00a038(5), 338\u2013349 (2003)","journal-title":"SIGPLAN Not."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Freund, S.N., Qadeer, S.: Checking concise specifications for multithreaded software. Journal of Object Technology\u00a03 (2004)","DOI":"10.5381\/jot.2004.3.6.a4"},{"issue":"4","key":"2_CR10","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1109\/TSE.2005.47","volume":"31","author":"S.N. Freund","year":"2005","unstructured":"Freund, S.N., Qadeer, S., Flanagan, C.: Exploiting purity for atomicity. IEEE Trans. Softw. Eng.\u00a031(4), 275\u2013291 (2005)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"2_CR11","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci.\u00a082(2), 253\u2013284 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR12","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2008.06.002","volume":"214","author":"W.H. Hesselink","year":"2008","unstructured":"Hesselink, W.H.: Simulation refinement for concurrency verification. Electr. Notes Theor. Comput. Sci.\u00a0214, 3\u201323 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-45694-5_8","volume-title":"CONCUR 2002 - Concurrency Theory","author":"Y. Kesten","year":"2002","unstructured":"Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.D.: Network invariants in action. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 101\u2013115. Springer, Heidelberg (2002)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/11817963_44","volume-title":"Computer Aided Verification","author":"R. Colvin","year":"2006","unstructured":"Colvin, R., Groves, L., Luchangco, V., Moir, M.: Formal verification of a lazy concurrent list-based set algorithm. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 475\u2013488. Springer, Heidelberg (2006)"},{"key":"2_CR15","first-page":"219","volume":"2","author":"N.A. Lynch","year":"1989","unstructured":"Lynch, N.A., Tuttle, M.R.: An introduction to input\/output automata. CWI Quarterly\u00a02, 219\u2013246 (1989)","journal-title":"CWI Quarterly"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/BFb0014319","volume-title":"Algebraic Methodology and Software Technology","author":"M. Marcus","year":"1996","unstructured":"Marcus, M., Pnueli, A.: Using ghost variables to prove refinement. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol.\u00a01101, pp. 226\u2013240. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15057-9_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:01:00Z","timestamp":1606186860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15057-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642150562","9783642150579"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15057-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}