{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:37Z","timestamp":1763468137874},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642397981"},{"type":"electronic","value":"9783642397998"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_68","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T19:13:06Z","timestamp":1373483586000},"page":"951-967","source":"Crossref","is-referenced-by-count":17,"title":["Efficient Synthesis for Concurrency by Semantics-Preserving Transformations"],"prefix":"10.1007","author":[{"given":"Pavol","family":"\u010cern\u00fd","sequence":"first","affiliation":[]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]},{"given":"Arjun","family":"Radhakrishna","sequence":"additional","affiliation":[]},{"given":"Leonid","family":"Ryzhyk","sequence":"additional","affiliation":[]},{"given":"Thorsten","family":"Tarrach","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"68_CR1","unstructured":"Poirot: The concurrency sleuth, \n                    \n                      http:\/\/research.microsoft.com\/en-us\/projects\/poirot\/"},{"key":"68_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 184\u2013190. Springer, Heidelberg (2011)"},{"key":"68_CR3","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":"68_CR4","doi-asserted-by":"crossref","unstructured":"Chou, A., Yang, J., Chelf, B., Hallem, S., Engler, D.: An empirical study of operating systems errors. In: SOSP, pp. 73\u201388 (2001)","DOI":"10.1145\/502059.502042"},{"key":"68_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"68_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-32759-9_17","volume-title":"FM 2012: Formal Methods","author":"E. Ermis","year":"2012","unstructured":"Ermis, E., Sch\u00e4f, M., Wies, T.: Error invariants. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol.\u00a07436, pp. 187\u2013201. Springer, Heidelberg (2012)"},{"key":"68_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-25318-8_16","volume-title":"Programming Languages and Systems","author":"A. Gupta","year":"2011","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Solving recursion-free horn clauses over LI+UIF. In: Yang, H. (ed.) APLAS 2011. LNCS, vol.\u00a07078, pp. 188\u2013203. Springer, Heidelberg (2011)"},{"key":"68_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-22110-1_32","volume-title":"Computer Aided Verification","author":"A. Gupta","year":"2011","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Threader: A constraint-based verifier for multi-threaded programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 412\u2013417. Springer, Heidelberg (2011)"},{"issue":"12","key":"68_CR9","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"R. Lipton","year":"1975","unstructured":"Lipton, R.: Reduction: A method of proving properties of parallel programs. Commun. ACM\u00a018(12), 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"key":"68_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/3-540-17906-2_30","volume-title":"Advances in Petri Nets 1986. Proceedings of an Advanced Course, Bad Honnef, 8.-19. September 1986","author":"A. Mazurkiewicz","year":"1987","unstructured":"Mazurkiewicz, A.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol.\u00a0255, pp. 278\u2013324. Springer, Heidelberg (1987)"},{"key":"68_CR11","unstructured":"Nielson, F., Nielson, H., Hankin, C.: Principles of program analysis (2. corr. print). Springer (2005)"},{"key":"68_CR12","doi-asserted-by":"crossref","unstructured":"Ryzhyk, L., Chubb, P., Kuz, I., Heiser, G.: Dingo: Taming device drivers. In: Eurosys (2009)","DOI":"10.1145\/1519065.1519095"},{"key":"68_CR13","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":"68_CR14","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E.: Deriving linearizable fine-grained concurrent objects. In: PLDI, pp. 125\u2013135 (2008)","DOI":"10.1145\/1379022.1375598"},{"key":"68_CR15","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"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_68","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T14:26:12Z","timestamp":1557930372000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_68"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_68","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}