{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T06:34:28Z","timestamp":1742970868064,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319216676"},{"type":"electronic","value":"9783319216683"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21668-3_11","type":"book-chapter","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T11:08:53Z","timestamp":1436785733000},"page":"180-197","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis"],"prefix":"10.1007","author":[{"given":"Pavol","family":"\u010cern\u00fd","sequence":"first","affiliation":[]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]},{"given":"Arjun","family":"Radhakrishna","sequence":"additional","affiliation":[]},{"given":"Leonid","family":"Ryzhyk","sequence":"additional","affiliation":[]},{"given":"Roopsha","family":"Samanta","sequence":"additional","affiliation":[]},{"given":"Thorsten","family":"Tarrach","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"508","DOI":"10.1007\/978-3-319-08867-9_33","volume-title":"Computer Aided Verification","author":"J Alglave","year":"2014","unstructured":"Alglave, J., Kroening, D., Nimal, V., Poetzl, D.: Don\u2019t sit on the fence. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 508\u2013524. Springer, Heidelberg (2014)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/BFb0012757","volume-title":"Automata, Languages and Programming","author":"A Bertoni","year":"1982","unstructured":"Bertoni, A., Mauri, G., Sabadini, N.: Equivalence and membership problems for regular trace languages. In: Nielsen, M., Schmidt, E.M. (eds.) Automata, Languages and Programming. LNCS, pp. 61\u201371. Springer, Heidelberg (1982)"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Bloem, R., Hofferek, G., K\u00f6nighofer, B., K\u00f6nighofer, R., Au\u00dferlechner, S., Sp\u00f6rk, R.: Synthesis of synchronization using uninterpreted functions. In: FMCAD, pp. 35\u201342 (2014)","DOI":"10.1109\/FMCAD.2014.6987593"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"951","DOI":"10.1007\/978-3-642-39799-8_68","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2013","unstructured":"\u010cern\u00fd, P., Henzinger, T.A., Radhakrishna, A., Ryzhyk, L., Tarrach, T.: Efficient synthesis for concurrency by semantics-preserving transformations. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 951\u2013967. Springer, Heidelberg (2013)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"568","DOI":"10.1007\/978-3-319-08867-9_38","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2014","unstructured":"\u010cern\u00fd, P., Henzinger, T.A., Radhakrishna, A., Ryzhyk, L., Tarrach, T.: Regression-free synthesis for concurrency. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 568\u2013584. Springer, Heidelberg (2014)"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Cherem, S., Chilimbi, T., Gulwani, S.: Inferring locks for atomic sections. In: PLDI, pp. 304\u2013315 (2008)","DOI":"10.1145\/1379022.1375619"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"11_CR8","volume-title":"Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. Springer, Heidelberg (1982)"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/11817963_5","volume-title":"Computer Aided Verification","author":"M Wulf De","year":"2006","unstructured":"De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: a new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17\u201330. Springer, Heidelberg (2006)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/978-3-642-11957-6_13","volume-title":"Programming Languages and Systems","author":"J Deshmukh","year":"2010","unstructured":"Deshmukh, J., Ramalingam, G., Ranganath, V.-P., Vaswani, K.: Logical concurrency control from sequential proofs. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 226\u2013245. Springer, Heidelberg (2010)"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Gupta, A., Henzinger, T., Radhakrishna, A., Samanta, R., Tarrach, T.: Succinct representation of concurrent trace sets. In: POPL15, pp. 433\u2013444 (2015)","DOI":"10.1145\/2775051.2677008"},{"key":"11_CR12","unstructured":"Jin, G., Zhang, W., Deng, D., Liblit, B., Lu, S.: Automated Concurrency-Bug Fixing. In: OSDI, pp. 221\u2013236 (2012)"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Ryzhyk, L., Chubb, P., Kuz, I., Heiser, G.: Dingo: Taming device drivers. In: Eurosys April 2009","DOI":"10.1145\/1519065.1519095"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Sadowski, C., Yi, J.: User evaluation of correctness conditions: A case study of cooperability. In: PLATEAU, pp. 2:1\u20132:6 (2010)","DOI":"10.1145\/1937117.1937119"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C., Bod\u00edk, R.: Sketching concurrent data structures. In: PLDI, pp. 136\u2013148 (2008)","DOI":"10.1145\/1379022.1375599"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: POPL, pp. 327\u2013338 (2010)","DOI":"10.1145\/1707801.1706338"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/978-3-642-15769-1_28","volume-title":"Static Analysis","author":"M Vechev","year":"2010","unstructured":"Vechev, M., Yahav, E., Raman, R., Sarkar, V.: Automatic verification of determinism for structured parallel programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 455\u2013471. Springer, Heidelberg (2010)"},{"key":"11_CR18","unstructured":"From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis (full version). \n                      http:\/\/arxiv.org\/abs\/1505.04533"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21668-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T20:13:54Z","timestamp":1563826434000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21668-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216676","9783319216683"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"14 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}