{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:25:10Z","timestamp":1740108310107,"version":"3.37.3"},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2018,7,2]],"date-time":"2018-07-02T00:00:00Z","timestamp":1530489600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Computing"],"published-print":{"date-parts":[[2019,1]]},"DOI":"10.1007\/s00607-018-0635-4","type":"journal-article","created":{"date-parts":[[2018,7,2]],"date-time":"2018-07-02T10:24:03Z","timestamp":1530527043000},"page":"59-74","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A mechanized refinement proof of the Chase\u2013Lev deque using a proof system"],"prefix":"10.1007","volume":"101","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0734-7969","authenticated-orcid":false,"given":"Suha Orhun","family":"Mutluergil","sequence":"first","affiliation":[]},{"given":"Serdar","family":"Tasiran","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,2]]},"reference":[{"issue":"2","key":"635_CR1","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/s00224-001-0004-z","volume":"34","author":"NS Arora","year":"2001","unstructured":"Arora NS, Blumofe RD, Plaxton CG (2001) Thread scheduling for multiprogrammed multiprocessors. Theory Comput Syst 34(2):115\u2013144","journal-title":"Theory Comput Syst"},{"key":"635_CR2","doi-asserted-by":"crossref","unstructured":"Chase D, Lev Y (2005) Dynamic circular work-stealing deque. In: Proceedings of the seventeenth annual ACM symposium on parallelism in algorithms and architectures. ACM, pp 21\u201328","DOI":"10.1145\/1073970.1073974"},{"issue":"1","key":"635_CR3","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/2775051.2676963","volume":"50","author":"M Dodds","year":"2015","unstructured":"Dodds M, Haas A, Kirsch CM (2015) A scalable, correct time-stamped stack. ACM SIGPLAN Not 50(1):233\u2013246","journal-title":"ACM SIGPLAN Not"},{"key":"635_CR4","doi-asserted-by":"crossref","unstructured":"Elmas T, Qadeer S, Tasiran S (2009) A calculus of atomic actions. In: ACM symposium on principles of programming languages. Association for Computing Machinery, Inc., p\u00a014. http:\/\/research.microsoft.com\/apps\/pubs\/default.aspx?id=70608 . Retrieved 25 Sept 2017","DOI":"10.1145\/1594834.1480885"},{"key":"635_CR5","doi-asserted-by":"crossref","unstructured":"Frigo M, Leiserson CE, Randall KH (1998) The implementation of the Cilk-5 multithreaded language. In: ACM Sigplan Notices. ACM, vol\u00a033, pp 212\u2013223","DOI":"10.1145\/277652.277725"},{"key":"635_CR6","doi-asserted-by":"crossref","unstructured":"Hawblitzel C, Qadeer S, Tasiran S (2015) Automated and modular refinement reasoning for concurrent programs. In: Computer aided verification","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"635_CR7","doi-asserted-by":"crossref","unstructured":"Herlihy M, Luchangco V, Moir M (2003) Obstruction-free synchronization: Double-ended queues as an example. In: Distributed computing systems, 2003. Proceedings. 23rd international conference on, IEEE, pp 522\u2013529","DOI":"10.1109\/ICDCS.2003.1203503"},{"key":"635_CR8","unstructured":"Khorsandi\u00a0Aghai M (2012) Verification of work-stealing deque implementation. Master\u2019s thesis, Uppsala University"},{"key":"635_CR9","unstructured":"L\u00ea NM, Pop A, Cohen A, Zappa\u00a0Nardelli F (2013) Correct and efficient work-stealing for weak memory models. In: ACM SIGPLAN Notices, vol\u00a048. ACM, pp 69\u201380"},{"issue":"12","key":"635_CR10","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton RJ (1975) Reduction: a method of proving properties of parallel programs. Commun ACM 18(12):717\u2013721","journal-title":"Commun ACM"},{"key":"635_CR11","doi-asserted-by":"crossref","unstructured":"Liu F, Nedev N, Prisadnikov N, Vechev M, Yahav E (2012) Dynamic synthesis for relaxed memory models. In: ACM SIGPLAN Notices, vol\u00a047. ACM, pp 429\u2013440","DOI":"10.1145\/2345156.2254115"},{"key":"635_CR12","doi-asserted-by":"crossref","unstructured":"Michael MM, Vechev MT, Saraswat VA (2009) Idempotent work stealing, vol\u00a044. ACM","DOI":"10.1145\/1594835.1504186"},{"issue":"4","key":"635_CR13","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1145\/2644865.2541987","volume":"49","author":"A Morrison","year":"2014","unstructured":"Morrison A, Afek Y (2014) Fence-free work stealing on bounded TSO processors. ACM SIGPLAN Not 49(4):413\u2013426","journal-title":"ACM SIGPLAN Not"},{"issue":"4","key":"635_CR14","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S Owicki","year":"1976","unstructured":"Owicki S, Gries D (1976) An axiomatic proof technique for parallel programs I. Acta Inform 6(4):319\u2013340","journal-title":"Acta Inform"},{"key":"635_CR15","doi-asserted-by":"crossref","unstructured":"Travkin O, Wehrheim H (2014) Handling TSO in mechanized linearizability proofs. In: Haifa verification conference. Springer, pp 132\u2013147","DOI":"10.1007\/978-3-319-13338-6_11"}],"container-title":["Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00607-018-0635-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00607-018-0635-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00607-018-0635-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,4]],"date-time":"2020-11-04T22:15:52Z","timestamp":1604528152000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00607-018-0635-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,2]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,1]]}},"alternative-id":["635"],"URL":"https:\/\/doi.org\/10.1007\/s00607-018-0635-4","relation":{},"ISSN":["0010-485X","1436-5057"],"issn-type":[{"type":"print","value":"0010-485X"},{"type":"electronic","value":"1436-5057"}],"subject":[],"published":{"date-parts":[[2018,7,2]]},"assertion":[{"value":"26 September 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 June 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 July 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}