{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:26:00Z","timestamp":1740122760879,"version":"3.37.3"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2016,9,27]],"date-time":"2016-09-27T00:00:00Z","timestamp":1474934400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2016,9,27]],"date-time":"2016-09-27T00:00:00Z","timestamp":1474934400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["267989"],"award-info":[{"award-number":["267989"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11402-N23","Z211-N23"],"award-info":[{"award-number":["S11402-N23","Z211-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF 1421752"],"award-info":[{"award-number":["CCF 1421752"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000893","name":"Simons Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000893","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100002418","name":"Intel Corporation","doi-asserted-by":"publisher","award":["gift"],"award-info":[{"award-number":["gift"]}],"id":[{"id":"10.13039\/100002418","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF 1138996"],"award-info":[{"award-number":["CCF 1138996"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s10703-016-0256-5","type":"journal-article","created":{"date-parts":[[2016,9,27]],"date-time":"2016-09-27T17:39:45Z","timestamp":1474997985000},"page":"97-139","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["From non-preemptive to preemptive scheduling using synchronization synthesis"],"prefix":"10.1007","volume":"50","author":[{"given":"Pavol","family":"\u010cern\u00fd","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arjun","family":"Radhakrishna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonid","family":"Ryzhyk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roopsha","family":"Samanta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4409-8487","authenticated-orcid":false,"given":"Thorsten","family":"Tarrach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,9,27]]},"reference":[{"key":"256_CR1","unstructured":"Alglave J, Kroening D, Nimal V, Poetzl D (2014) Don\u2019t sit on the fence\u2014a static analysis approach to automatic fence insertion. In: CAV, pp 508\u2013524"},{"key":"256_CR2","doi-asserted-by":"crossref","unstructured":"Bertoni A, Mauri G, Sabadini N (1982) Equivalence and membership problems for regular trace languages. In: Automata, languages and programming. Springer, Heidelberg, pp 61\u201371","DOI":"10.1007\/BFb0012757"},{"key":"256_CR3","doi-asserted-by":"crossref","unstructured":"Bloem R, Hofferek G, K\u00f6nighofer B, K\u00f6nighofer R, Au\u00dferlechner S, Sp\u00f6rk R (2014) Synthesis of synchronization using uninterpreted functions. In: FMCAD, pp 35\u201342","DOI":"10.1109\/FMCAD.2014.6987593"},{"key":"256_CR4","doi-asserted-by":"crossref","unstructured":"\u010cern\u00fd P, Clarke EM, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach T (2013) From non-preemptive to preemptive scheduling using synchronization synthesis. In: CAV, pp 180\u2013197. \n                    https:\/\/github.com\/thorstent\/Liss","DOI":"10.1007\/978-3-319-21668-3_11"},{"key":"256_CR5","doi-asserted-by":"crossref","unstructured":"\u010cern\u00fd P, Henzinger T, Radhakrishna A, Ryzhyk L, Tarrach T (2013) Efficient synthesis for concurrency by semantics-preserving transformations. In: CAV, pp 951\u2013967","DOI":"10.1007\/978-3-642-39799-8_68"},{"key":"256_CR6","doi-asserted-by":"crossref","unstructured":"\u010cern\u00fd P, Henzinger T, Radhakrishna A, Ryzhyk L, Tarrach T (2014) Regression-free synthesis for concurrency. In: CAV, pp 568\u2013584. \n                    https:\/\/github.com\/thorstent\/ConRepair","DOI":"10.1007\/978-3-319-08867-9_38"},{"key":"256_CR7","unstructured":"\u010cern\u00fd P, Clarke EM, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach T (2015) Optimizing solution quality in synchronization synthesis. ArXiv e-prints. \n                    ArXiv:1511.07163"},{"key":"256_CR8","doi-asserted-by":"crossref","unstructured":"Cherem S, Chilimbi T, Gulwani S (2008) Inferring locks for atomic sections. In: PLDI, pp 304\u2013315","DOI":"10.1145\/1375581.1375619"},{"key":"256_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774","volume-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"EM Clarke","year":"1982","unstructured":"Clarke EM, Emerson EA (1982) Design and synthesis of synchronization skeletons using branching time temporal logic. Springer, Berlin"},{"key":"256_CR10","doi-asserted-by":"crossref","unstructured":"Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: TACAS, pp 168\u2013176. \n                    http:\/\/www.cprover.org\/cbmc\/","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"256_CR11","doi-asserted-by":"crossref","unstructured":"De\u00a0Wulf M, Doyen L, Henzinger TA, Raskin JF (2006) Antichains: a new algorithm for checking universality of finite automata. In: CAV. Springer, Heidelberg, pp 17\u201330","DOI":"10.1007\/11817963_5"},{"key":"256_CR12","doi-asserted-by":"crossref","unstructured":"Deshmukh J, Ramalingam G, Ranganath V, Vaswani K (2010) Logical concurrency control from sequential proofs. In: Programming languages and systems. Springer, Heidelberg, pp 226\u2013245","DOI":"10.1007\/978-3-642-11957-6_13"},{"issue":"11","key":"256_CR13","doi-asserted-by":"publisher","first-page":"624","DOI":"10.1145\/360363.360369","volume":"19","author":"KP Eswaran","year":"1976","unstructured":"Eswaran KP, Gray JN, Lorie RA, Traiger IL (1976) The notions of consistency and predicate locks in a database system. Commun ACM 19(11):624\u2013633","journal-title":"Commun ACM"},{"key":"256_CR14","doi-asserted-by":"crossref","unstructured":"Flanagan C, Qadeer S (2003) Types for atomicity. In: ACM SIGPLAN notices, vol 38. ACM, New York, pp 1\u201312","DOI":"10.1145\/604174.604176"},{"key":"256_CR15","doi-asserted-by":"crossref","unstructured":"Gupta A, Henzinger T, Radhakrishna A, Samanta R, Tarrach T (2015) Succinct representation of concurrent trace sets. In: POPL15, pp 433\u2013444","DOI":"10.1145\/2676726.2677008"},{"issue":"3","key":"256_CR16","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"MP Herlihy","year":"1990","unstructured":"Herlihy MP, Wing JM (1990) Linearizability: a correctness condition for concurrent objects. ACM Trans Progr Lang Syst (TOPLAS) 12(3):463\u2013492","journal-title":"ACM Trans Progr Lang Syst (TOPLAS)"},{"key":"256_CR17","unstructured":"Jin G, Zhang W, Deng D, Liblit B, Lu S (2012) Automated concurrency-bug fixing. In: OSDI, pp 221\u2013236"},{"key":"256_CR18","doi-asserted-by":"crossref","unstructured":"Khoshnood S, Kusano M, Wang C (2015) ConcBugAssist: constraint solving for diagnosis and repair of concurrency bugs. In: International symposium on software testing and analysis","DOI":"10.1145\/2771783.2771798"},{"key":"256_CR19","unstructured":"Memcached distributed memory object caching system. \n                    http:\/\/memcached.org\n                    \n                  . Accessed 01 Jul 2015"},{"key":"256_CR20","volume-title":"The theory of database concurrency control","author":"C Papadimitriou","year":"1986","unstructured":"Papadimitriou C (1986) The theory of database concurrency control. Computer Science Press, Rockville"},{"key":"256_CR21","doi-asserted-by":"crossref","unstructured":"Ryzhyk L, Chubb P, Kuz I, Heiser G (2009) Dingo: Taming device drivers. In: Eurosys","DOI":"10.1145\/1519065.1519095"},{"key":"256_CR22","doi-asserted-by":"crossref","unstructured":"Sadowski C, Yi J (2010) User evaluation of correctness conditions: a case study of cooperability. In: PLATEAU, pp 2:1\u20132:6","DOI":"10.1145\/1937117.1937119"},{"key":"256_CR23","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A, Jones C, Bod\u00edk R (2008) Sketching concurrent data structures. In: PLDI, pp 136\u2013148","DOI":"10.1145\/1375581.1375599"},{"key":"256_CR24","doi-asserted-by":"crossref","unstructured":"Vechev M, Yahav E, Yorsh G (2010) Abstraction-guided synthesis of synchronization. In: POPL, pp 327\u2013338","DOI":"10.1145\/1706299.1706338"},{"key":"256_CR25","doi-asserted-by":"crossref","unstructured":"Vechev MT, Yahav E, Raman R, Sarkar V (2010) Automatic verification of determinism for structured parallel programs. In: SAS, pp 455\u2013471","DOI":"10.1007\/978-3-642-15769-1_28"},{"key":"256_CR26","doi-asserted-by":"crossref","unstructured":"Yi J, Flanagan C (2010) Effects for cooperable and serializable threads. In: Proceedings of the 5th ACM SIGPLAN workshop on types in language design and implementation. ACM, New York, pp 3\u201314","DOI":"10.1145\/1708016.1708019"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0256-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-016-0256-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0256-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T15:43:48Z","timestamp":1589730228000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-016-0256-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,27]]},"references-count":26,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["256"],"URL":"https:\/\/doi.org\/10.1007\/s10703-016-0256-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2016,9,27]]},"assertion":[{"value":"27 September 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}