{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T03:42:50Z","timestamp":1752982970649,"version":"3.37.3"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2018,8,21]],"date-time":"2018-08-21T00:00:00Z","timestamp":1534809600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["678177"],"award-info":[{"award-number":["678177"]}],"id":[{"id":"10.13039\/501100000781","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":[[2019,8]]},"DOI":"10.1007\/s10703-018-0322-2","type":"journal-article","created":{"date-parts":[[2018,8,21]],"date-time":"2018-08-21T05:29:59Z","timestamp":1534829399000},"page":"4-26","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Abstract semantic diffing of evolving concurrent programs"],"prefix":"10.1007","volume":"54","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2727-8865","authenticated-orcid":false,"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[]},{"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,8,21]]},"reference":[{"issue":"2","key":"322_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M Abadi","year":"1991","unstructured":"Abadi M, Lamport L (1991) The existence of refinement mappings. Theor Comput Sci 82(2):253\u2013284","journal-title":"Theor Comput Sci"},{"key":"322_CR2","doi-asserted-by":"crossref","unstructured":"Biere A, Bloem R (eds) (2014) Computer aided verification\u2014CAV 2014, Vienna, Austria, 2014. Proceedings, volume 8559 of LNCS. Springer, Berlin","DOI":"10.1007\/978-3-319-08867-9"},{"key":"322_CR3","unstructured":"Bouajjani A, Derevenetc E, Meyer R (2014) Robustness against relaxed memory models. In: Hasselbring W, Ehmke NC (eds) Software engineering, Kiel, Deutschland, volume 227 of LNI, pp 85\u201386"},{"key":"322_CR4","doi-asserted-by":"crossref","unstructured":"Burckhardt S, Musuvathi M (2008) Effective program verification for relaxed memory models. In: CAV 2008, pp 107\u2013120","DOI":"10.1007\/978-3-540-70545-1_12"},{"issue":"2\u20133","key":"322_CR5","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10703-016-0256-5","volume":"50","author":"P Cern\u00fd","year":"2017","unstructured":"Cern\u00fd P, Clarke EM, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach T (2017) From non-preemptive to preemptive scheduling using synchronization synthesis. Form Methods Syst Des 50(2\u20133):97\u2013139","journal-title":"Form Methods Syst Des"},{"key":"322_CR6","first-page":"951","volume-title":"computer aided verification \u2014CAV 2013, Saint Petersburg, 2013, volume 8044 of lecture notes in computer science","author":"P Cern\u00fd","year":"2013","unstructured":"Cern\u00fd P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T (2013) Efficient synthesis for concurrency by semantics-preserving transformations. In: Sharygina N, Veith H (eds) computer aided verification \u2014CAV 2013, Saint Petersburg, 2013, volume 8044 of lecture notes in computer science. Springer, Berlin, pp 951\u2013967"},{"key":"322_CR7","doi-asserted-by":"crossref","unstructured":"Cern\u00fd P, Henzinger TA, Arjun R, Leonid R, Thorsten T Regression-free synthesis for concurrency. In: Biere and Bloem [2], pp 568\u2013584","DOI":"10.1007\/978-3-319-08867-9_38"},{"issue":"3","key":"322_CR8","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/s10703-015-0237-0","volume":"47","author":"S Chaki","year":"2015","unstructured":"Chaki S, Gurfinkel A, Strichman O (2015) Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation). Form Methods Syst Des 47(3):287\u2013301","journal-title":"Form Methods Syst Des"},{"key":"322_CR9","first-page":"168","volume-title":"Tools and algorithms for the construction and analysis of systems (TACAS 2004), volume 2988 of LNCS","author":"E Clarke","year":"2004","unstructured":"Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Jensen K, Podelski A (eds) Tools and algorithms for the construction and analysis of systems (TACAS 2004), volume 2988 of LNCS. Springer, Berlin, pp 168\u2013176"},{"key":"322_CR10","doi-asserted-by":"crossref","unstructured":"Farzan A, Kincaid Z, Podelski A (2013) Inductive data flow graphs. In: Giacobazzi R, Cousot R (eds) The 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL \u201913, Rome, Italy, 23\u201325 January 2013. ACM, pp 129\u2013142","DOI":"10.1145\/2429069.2429086"},{"issue":"6","key":"322_CR11","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/s00236-008-0075-2","volume":"45","author":"B Godlin","year":"2008","unstructured":"Godlin B, Strichman O (2008) Inference rules for proving the equivalence of recursive procedures. Acta Inf 45(6):403\u2013439","journal-title":"Acta Inf"},{"key":"322_CR12","doi-asserted-by":"crossref","unstructured":"Inverso O, Nguyen TL, Fischer B, Torre La S, Parlato G (2015) Lazy-cseq: a context-bounded model checking tool for multi-threaded c-programs. In: Cohen MB, Grunske L, Whalen M (eds) 30th IEEE\/ACM international conference on automated software engineering, ASE 2015, Lincoln, NE, USA, 9\u201313 Nov 2015. IEEE Computer Society, pp 807\u2013812","DOI":"10.1109\/ASE.2015.108"},{"key":"322_CR13","doi-asserted-by":"crossref","unstructured":"Inverso O, Tomasco E, Fischer B, Torre La S, Parlato G Bounded model checking of multi-threaded C programs via lazy sequentialization. In: Biere and Bloem [2], pp 585\u2013602","DOI":"10.1007\/978-3-319-08867-9_39"},{"key":"322_CR14","doi-asserted-by":"crossref","unstructured":"Jackson D, Ladd DA (1994) Semantic diff: a tool for summarizing the effects of modifications. In: Proceedings of the international conference on software maintenance, ICSM 1994, Victoria, BC, Canada, Sept 1994. IEEE Computer Society, pp 243\u2013252","DOI":"10.1109\/ICSM.1994.336770"},{"key":"322_CR15","doi-asserted-by":"crossref","unstructured":"Joshi S, Lahiri SK, Lal A (2012) Underspecified harnesses and interleaved bugs. In: Field J, Hicks M (eds) Proceedings of the 39th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2012, Philadelphia, Pennsylvania, USA, 22\u201328 January 2012. ACM, pp 19\u201330","DOI":"10.1145\/2103656.2103662"},{"key":"322_CR16","doi-asserted-by":"crossref","unstructured":"Lahiri SK, Hawblitzel C, Kawaguchi M, Reb\u00ealo H (2012) Symdiff: a language-agnostic semantic diff tool for imperative programs. In: Proceedings of the 24th international conference on computer aided verification, CAV\u201912","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"322_CR17","doi-asserted-by":"crossref","unstructured":"Lahiri SK, McMillan KL, Sharma R, Hawblitzel C (2013) Differential assertion checking. In: Joint meeting of the european software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering, ESEC\/FSE\u201913, Saint Petersburg, Russian Federation, 18\u201326 Aug 2013. ACM, pp 345\u2013355","DOI":"10.1145\/2491411.2491452"},{"key":"322_CR18","doi-asserted-by":"crossref","unstructured":"Logozzo F, Lahiri SK, F\u00e4hndrich M, Blackshear S (2014) Verification modulo versions: towards usable verification. In: ACM SIGPLAN conference on programming language design and implementation, PLDI \u201914, Edinburgh, United Kingdom, 09\u201311 June 2014. ACM, p 32","DOI":"10.1145\/2666356.2594326"},{"key":"322_CR19","doi-asserted-by":"crossref","unstructured":"Lu S, Park S, Seo E, Zhou Y (2008) Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: Eggers SJ, Larus JR (eds) Proceedings of the 13th international conference on architectural support for programming languages and operating systems, ASPLOS 2008, Seattle, WA, USA, 1\u20135 Mar 2008. ACM, pp 329\u2013339","DOI":"10.1145\/1346281.1346323"},{"key":"322_CR20","unstructured":"Marinescu PD, Cadar C (2013) KATCH: high-coverage testing of software patches. In: Joint meeting of the european software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering, ESEC\/FSE\u201913, Saint Petersburg, Russian Federation, 18\u201326 Aug 2013. ACM, pp 235\u2013245"},{"key":"322_CR21","doi-asserted-by":"crossref","unstructured":"Person S, Dwyer MB, Elbaum SG, Pasareanu CS (2008) Differential symbolic execution. In: Proceedings of the 16th ACM SIGSOFT international symposium on foundations of software engineering, 2008, Atlanta, Georgia, USA, 9\u201314 Nov 2008. ACM, pp 226\u2013237","DOI":"10.1145\/1453101.1453131"},{"key":"322_CR22","doi-asserted-by":"crossref","unstructured":"Rosen BK, Wegman MN, Zadeck FK (1988) Global value numbers and redundant computations. In: Ferrante J, Mager P (eds) Conference record of the fifteenth annual ACM symposium on principles of programming languages, San Diego, California, USA, 10\u201313 Jan 1988. ACM Press, pp 12\u201327","DOI":"10.1145\/73560.73562"},{"issue":"2","key":"322_CR23","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1145\/42190.42277","volume":"10","author":"D Shasha","year":"1988","unstructured":"Shasha D, Snir M (1988) Efficient and correct execution of parallel programs that share memory. ACM Trans Program Lang Syst 10(2):282\u2013312","journal-title":"ACM Trans Program Lang Syst"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-0322-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-018-0322-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-0322-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,20]],"date-time":"2019-09-20T00:39:17Z","timestamp":1568939957000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-018-0322-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,8,21]]},"references-count":23,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,8]]}},"alternative-id":["322"],"URL":"https:\/\/doi.org\/10.1007\/s10703-018-0322-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2018,8,21]]},"assertion":[{"value":"21 August 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}