{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:57:39Z","timestamp":1770274659663,"version":"3.49.0"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2012,5,23]],"date-time":"2012-05-23T00:00:00Z","timestamp":1337731200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2013,10]]},"DOI":"10.1007\/s10009-012-0232-3","type":"journal-article","created":{"date-parts":[[2012,7,8]],"date-time":"2012-07-08T01:41:37Z","timestamp":1341711697000},"page":"413-431","source":"Crossref","is-referenced-by-count":8,"title":["Abstraction-guided synthesis of synchronization"],"prefix":"10.1007","volume":"15","author":[{"given":"Martin","family":"Vechev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eran","family":"Yahav","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Greta","family":"Yorsh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,5,23]]},"reference":[{"key":"232_CR1","doi-asserted-by":"crossref","unstructured":"Attie, P., Emerson, E.: Synthesis of concurrent systems for an atomic read\/atomic write model of computation, pp. 111\u2013120. In: PODC \u201996, ACM, Berlin (1996)","DOI":"10.1145\/248052.248070"},{"key":"232_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: SPIN, pp. 103\u2013122 (2001)","DOI":"10.1007\/3-540-45139-0_7"},{"key":"232_CR3","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI, pp. 196\u2013207 (2003)","DOI":"10.1145\/780822.781153"},{"key":"232_CR4","doi-asserted-by":"crossref","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: CAV, pp. 140\u2013156 (2009)","DOI":"10.1007\/978-3-642-02658-4_14"},{"key":"232_CR5","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":"232_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, Workshop, pp. 52\u201371 (1982)","DOI":"10.1007\/BFb0025774"},{"key":"232_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV, pp. 154\u2013169 (2000)","DOI":"10.1007\/10722167_15"},{"key":"232_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"232_CR9","doi-asserted-by":"crossref","unstructured":"Emmi, M., Fischer, J.S., Jhala, R., Majumdar, R.: Lock allocation. In: POPL, pp. 291\u2013296 (2007)","DOI":"10.1145\/1190215.1190260"},{"key":"232_CR10","doi-asserted-by":"crossref","unstructured":"Golan-Gueta, G., Bronson, N., Aiken, A., Ramalingam, G., Sagiv, M., Yahav, E.: Automatic fine-grain locking using shape properties. In: Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, pp. 225\u2013242. OOPSLA \u201911. ACM, New York (2011)","DOI":"10.1145\/2048066.2048086"},{"key":"232_CR11","doi-asserted-by":"crossref","unstructured":"Griesmayer, A., Bloem, R.P., Cook, B.: Repair of boolean programs with an application to C. In: CAV, pp. 358\u2013371 (2006)","DOI":"10.1007\/11817963_33"},{"key":"232_CR12","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/565816.503279"},{"key":"232_CR13","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: CAV, pp. 226\u2013238 (2005)","DOI":"10.1007\/11513988_23"},{"key":"232_CR14","unstructured":"Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. J. Comput. Syst. Sci. (2008)"},{"key":"232_CR15","unstructured":"Kuperstein, M.: Preserving correctness under relaxed memory models. Master\u2019s thesis, Technion (2012)"},{"key":"232_CR16","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Automatic fence inference. In: FMCAD\u201910: Formal Methods in Computer Aided Design (2010)"},{"key":"232_CR17","doi-asserted-by":"crossref","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Partial-coherence abstractions for relaxed memory models. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI \u201911, pp. 187\u2013198. ACM, New York (2011)","DOI":"10.1145\/1993498.1993521"},{"key":"232_CR18","doi-asserted-by":"crossref","unstructured":"Liu, F., Nedev, N., Prisadnikov, N., Vechev, M., Yahav, E.: Dynamic synthesis for relaxed memory models. In: PLDI\u201912: Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation (2012)","DOI":"10.1145\/2254064.2254115"},{"issue":"1","key":"232_CR19","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z. Manna","year":"1984","unstructured":"Manna Z., Wolper P.: Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst. 6(1), 68\u201393 (1984)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"232_CR20","doi-asserted-by":"crossref","unstructured":"McCloskey, B., Zhou, F., Gay, D., Brewer, E.: Autolocker: synchronization inference for atomic sections. In: POPL, pp. 346\u2013358 (2006)","DOI":"10.1145\/1111320.1111068"},{"issue":"1","key":"232_CR21","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9 A.: The octagon abstract domain. Higher Order Symbol. Comput. 19(1), 31\u2013100 (2006)","journal-title":"Higher Order Symbol. Comput."},{"key":"232_CR22","unstructured":"Nagpaly, R., Pattabiramanz, K., Kirovski, D., Zorn, B.: Tolerace: Tolerating and detecting races. In: STMCS: Second Workshop on Software Tools for Multi-Core Systems (2007)"},{"key":"232_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL \u201989, pp. 179\u2013190. ACM, New York (1989)","DOI":"10.1145\/75277.75293"},{"key":"232_CR24","unstructured":"Rajamani, S., Ramalingam, G., Ranganath, V.-P., Vaswani, K.: Controlling non-determinism for semantic guarantees. In: Exploiting Concurrency Efficiently and Correctly\u2014(EC)2 (2008)"},{"issue":"5","key":"232_CR25","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1145\/1275497.1275501","volume":"29","author":"X. Rival","year":"2007","unstructured":"Rival X., Mauborgne L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. 29(5), 26 (2007)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"232_CR26","doi-asserted-by":"crossref","unstructured":"Shavit, N., Touitou, D.: Software transactional memory. In: PODC \u201995, pp. 204\u2013213. ACM, New York (1995)","DOI":"10.1145\/224964.224987"},{"key":"232_CR27","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Arnold, G., Tancau, L., Bod\u00edk, R., Saraswat, V.A., Seshia, S.A.: Sketching stencils. In: PLDI, pp. 167\u2013178 (2007)","DOI":"10.1145\/1273442.1250754"},{"key":"232_CR28","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C.G., Bodik, R.: Sketching concurrent data structures. In: PLDI, pp. 136\u2013148 (2008)","DOI":"10.1145\/1379022.1375599"},{"key":"232_CR29","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Rabbah, R.M., Bod\u00edk, R., Ebcioglu, K.: Programming by Sketching for Bit-Streaming Programs. In: PLDI, pp. 281\u2013294 (2005)","DOI":"10.1145\/1064978.1065045"},{"key":"232_CR30","doi-asserted-by":"crossref","unstructured":"Staber, S., Jobstmann, B., Bloem, R.: Finding and fixing faults. In: CHARME, pp. 35\u201349 (2005)","DOI":"10.1007\/11560548_6"},{"key":"232_CR31","unstructured":"The SAT4J SAT solver. http:\/\/www.sat4j.org\/"},{"key":"232_CR32","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the Symposium on Logic in Computer Science, pp. 332\u2013344 (1986)"},{"key":"232_CR33","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":"232_CR34","doi-asserted-by":"crossref","unstructured":"Vechev, M.T., Yahav, E., Bacon, D.F., Rinetzky, N.: Cgcexplorer: a semi-automated search procedure for provably correct concurrent collectors. In: PLDI, pp. 456\u2013467 (2007)","DOI":"10.1145\/1273442.1250787"},{"key":"232_CR35","doi-asserted-by":"crossref","unstructured":"Vechev, M.T., Yahav, E., Yorsh, G.: Inferring synchronization under limited observability. In: TACAS, pp. 139\u2013154 (2009)","DOI":"10.1007\/978-3-642-00768-2_13"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0232-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0232-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0232-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,30]],"date-time":"2019-06-30T18:14:08Z","timestamp":1561918448000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0232-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,5,23]]},"references-count":35,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["232"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0232-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,5,23]]}}}