{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T19:49:44Z","timestamp":1773344984394,"version":"3.50.1"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319216898","type":"print"},{"value":"9783319216904","type":"electronic"}],"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-21690-4_18","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T06:08:27Z","timestamp":1436940507000},"page":"307-323","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["Learning Commutativity Specifications"],"prefix":"10.1007","author":[{"given":"Timon","family":"Gehr","sequence":"first","affiliation":[]},{"given":"Dimitar","family":"Dimitrov","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Vechev","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Attiya, H., Guerraoui, R., Hendler, D., Kuznetsov, P., Michael, M.M., Vechev, M.T.: Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26\u201328 Jan 2011 (2011)","DOI":"10.1145\/1926385.1926442"},{"key":"18_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511549809","volume-title":"Oligomorphic Permutation Groups","author":"PJ Cameron","year":"1990","unstructured":"Cameron, P.J.: Oligomorphic Permutation Groups. Cambridge University Press, Cambridge (1990)"},{"key":"18_CR3","volume-title":"Model Theory. Studies in Logic and the Foundations of Mathematics","author":"CC Chang","year":"1990","unstructured":"Chang, C.C., Keisler, H.J.: Model Theory. Studies in Logic and the Foundations of Mathematics. Elsevier Science, North-Holland (1990)"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Dimitrov, D., Raychev, V., Vechev, M.T., Koskinen, E.: Commutativity race detection. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI2014, Edinburgh, UK - 09\u201311 June 2014 (2014)","DOI":"10.1145\/2594291.2594322"},{"issue":"1\u20133","key":"18_CR5","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/978-3-319-08867-9_5","volume-title":"Computer Aided Verification","author":"P Garg","year":"2014","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE: A robust framework for learning invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69\u201387. Springer, Heidelberg (2014)"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Taly, A.: Automated synthesis of symbolic instruction encodings from i\/o samples. In: PLDI2012, pp. 441\u2013452, New York, ACM (2012)","DOI":"10.1145\/2345156.2254116"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-00768-2_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Gupta","year":"2009","unstructured":"Gupta, A., Majumdar, R., Rybalchenko, A.: From tests to proofs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 262\u2013276. Springer, Heidelberg (2009)"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Koskinen, E.: Transactional boosting: a methodology for highly-concurrent transactional objects. In: Proceedings of the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2008, Salt Lake City, UT, USA, 20\u201323 Feb 2008 (2008)","DOI":"10.1145\/1345206.1345237"},{"key":"18_CR10","volume-title":"Model Theory: Encyclopedia of Mathematics and its Applications","author":"W Hodges","year":"2008","unstructured":"Hodges, W.: Model Theory: Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge (2008)"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Proceedings of the 32Nd ACM\/IEEE International Conference on Software Engineering - Volume 1, ICSE\u20192010, pp. 215\u2013224, New York, NY, USA, ACM (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Kim, D., Rinard, M.C.: Verification of semantic commutativity conditions and inverse operations on linked data structures. In: PLDI\u20192011, pp. 528\u2013541, New York, NY, USA, ACM (2011)","DOI":"10.1145\/1993316.1993561"},{"issue":"6","key":"18_CR13","doi-asserted-by":"publisher","first-page":"542","DOI":"10.1145\/1993316.1993562","volume":"46","author":"M Kulkarni","year":"2011","unstructured":"Kulkarni, M., Nguyen, D., Prountzos, D., Sui, X., Pingali, K.: Exploiting the commutativity lattice. SIGPLAN Not. 46(6), 542\u2013555 (2011)","journal-title":"SIGPLAN Not."},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Kulkarni, M., Pingali, K., Walter, B., Ramanarayanan, G., Bala, K., Chew, L.P.: Optimistic parallelism requires abstractions. In: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, 10\u201313 June 2007 (2007)","DOI":"10.1145\/1250734.1250759"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Relevance heuristics for program analysis. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, 7\u201312 Jan 2008 (2008)","DOI":"10.1145\/1328438.1328440"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to generate disjunctive invariants. In: ICSE 2014, pp. 608\u2013619. ACM (2014)","DOI":"10.1145\/2568225.2568275"},{"key":"18_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8622-1","volume-title":"A Course in Model Theory: An Introduction to Contemporary Mathematical Logic Universitext","author":"B Poizat","year":"2000","unstructured":"Poizat, B.: A Course in Model Theory: An Introduction to Contemporary Mathematical Logic Universitext. Springer, New York (2000)"},{"issue":"5","key":"18_CR18","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1016\/0005-1098(78)90005-5","volume":"14","author":"J Rissanen","year":"1978","unstructured":"Rissanen, J.: Modeling by shortest data description. Automatica 14(5), 465\u2013471 (1978)","journal-title":"Automatica"},{"key":"18_CR19","volume-title":"Information and Complexity in Statistical Modeling","author":"J Rissanen","year":"2010","unstructured":"Rissanen, J.: Information and Complexity in Statistical Modeling. Springer, New York (2010)"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/978-3-319-08867-9_6","volume-title":"Computer Aided Verification","author":"R Sharma","year":"2014","unstructured":"Sharma, R., Aiken, A.: From invariant checking to invariant inference using randomized search. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 88\u2013105. Springer, Heidelberg (2014)"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-642-38856-9_21","volume-title":"Static Analysis","author":"R Sharma","year":"2013","unstructured":"Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Nori, A.V.: Verification as learning geometric concepts. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 388\u2013411. Springer, Heidelberg (2013)"},{"key":"18_CR22","volume-title":"Statistical Learning Theory. Adaptive and Learning Systems for Signal Processing, Communications, and Control","author":"VN Vapnik","year":"1998","unstructured":"Vapnik, V.N.: Statistical Learning Theory. Adaptive and Learning Systems for Signal Processing, Communications, and Control. Wiley, New York (1998)"},{"issue":"12","key":"18_CR23","doi-asserted-by":"publisher","first-page":"1488","DOI":"10.1109\/12.9728","volume":"37","author":"WE Weihl","year":"1988","unstructured":"Weihl, W.E.: Commutativity-based concurrency control for abstract data types. IEEE Trans. Comput. 37(12), 1488\u20131505 (1988)","journal-title":"IEEE Trans. Comput."}],"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-21690-4_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,18]],"date-time":"2022-05-18T03:09:40Z","timestamp":1652843380000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}