{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:02:07Z","timestamp":1762459327058,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662488980"},{"type":"electronic","value":"9783662488997"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_42","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"606-621","source":"Crossref","is-referenced-by-count":16,"title":["Automated Discovery of Simulation Between\u00a0Programs"],"prefix":"10.1007","author":[{"given":"Grigory","family":"Fedyukovich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"42_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1007\/978-3-642-31424-7_48","volume-title":"Computer Aided Verification","author":"A Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: a framework for abstraction- and interpolation-based software verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 672\u2013678. Springer, Heidelberg (2012)"},{"issue":"5","key":"42_CR2","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"42_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/978-3-319-11737-9_6","volume-title":"Formal Methods and Software Engineering","author":"\u015e Ciob\u00e2c\u0103","year":"2014","unstructured":"Ciob\u00e2c\u0103, \u015e., Lucanu, D., Rusu, V., Ro\u015fu, G.: A language-independent proof system for mutual program equivalence. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 75\u201390. Springer, Heidelberg (2014)"},{"key":"42_CR4","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. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"42_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55179-4_25","volume-title":"Computer Aided Verification","author":"DL Dill","year":"1992","unstructured":"Dill, D.L., Hu, A.J., Wong-Toi, H.: Checking for language inclusion using simulation preorders. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575. Springer, Heidelberg (1992)"},{"key":"42_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-319-06200-6_25","volume-title":"NASA Formal Methods","author":"G Fedyukovich","year":"2014","unstructured":"Fedyukovich, G., Gurfinkel, A., Sharygina, N.: Incremental verification of compiler optimizations. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 300\u2013306. Springer, Heidelberg (2014)"},{"key":"42_CR7","doi-asserted-by":"crossref","unstructured":"Felsing, D., Grebing, S., Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating regression verification. In: ASE, pp. 349\u2013360. ACM (2014)","DOI":"10.1145\/2642937.2642987"},{"key":"42_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-3-319-17524-9_13","volume-title":"NASA Formal Methods","author":"A Gacek","year":"2015","unstructured":"Gacek, A., Katis, A., Whalen, M.W., Backes, J., Cofer, D.: Towards realizability checking of contracts using theories. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 173\u2013187. Springer, Heidelberg (2015)"},{"key":"42_CR9","doi-asserted-by":"crossref","unstructured":"Gasc\u00f3n, A., Subramanyan, P., Dutertre, B., Tiwari, A., Jovanovic, D., Malik, S.: Template-based circuit understanding. In: FMCAD, pp. 83\u201390. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987599"},{"key":"42_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1007\/978-3-662-46081-8_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Gjomemo","year":"2015","unstructured":"Gjomemo, R., Namjoshi, K.S., Phung, P.H., Venkatakrishnan, V.N., Zuck, L.D.: From verification to optimizations. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 300\u2013317. Springer, Heidelberg (2015)"},{"key":"42_CR11","doi-asserted-by":"crossref","unstructured":"Henzinger, M.R., Henzinger, T.A., Kopke, P.: Computing simulations on finite and infinite graphs. In: FOCS, pp. 453\u2013462 (1995)","DOI":"10.1109\/SFCS.1995.492576"},{"key":"42_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/978-3-319-08867-9_2","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2014","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17\u201334. Springer, Heidelberg (2014)"},{"key":"42_CR13","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., McMillan, K.L., Sharma, R., Hawblitzel, C.: Differential assertion checking. In: FSE, pp. 345\u2013355. ACM (2013)","DOI":"10.1145\/2491411.2491452"},{"issue":"5","key":"42_CR14","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","volume":"36","author":"R Loos","year":"1993","unstructured":"Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J. 36(5), 450\u2013462 (1993)","journal-title":"Comput. J."},{"key":"42_CR15","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: IJCAI, pp. 481\u2013489 (1971)"},{"key":"42_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-540-89439-1_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Monniaux","year":"2008","unstructured":"Monniaux, D.: A quantifier elimination algorithm for linear real arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 243\u2013257. Springer, Heidelberg (2008)"},{"key":"42_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-38856-9_17","volume-title":"Static Analysis","author":"KS Namjoshi","year":"2013","unstructured":"Namjoshi, K.S., Zuck, L.D.: Witnessing program transformations. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 304\u2013323. Springer, Heidelberg (2013)"},{"key":"42_CR18","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI, pp. 83\u201394. ACM (2000)","DOI":"10.1145\/358438.349314"},{"key":"42_CR19","doi-asserted-by":"crossref","unstructured":"Phan, A.-D., Bj\u00f8rner, N., Monniaux, D.: Anatomy of alternating quantifier satisfiability (work in progress). In: SMT, EPiC Series, vol. 20, pp. 120\u2013130. EasyChair (2012)","DOI":"10.29007\/8cf7"},{"key":"42_CR20","first-page":"125","volume":"10","author":"T Skolem","year":"1928","unstructured":"Skolem, T.: \u00dcber die mathematische logik. Norsk Matematisk Tidsskrift 10, 125\u2013142 (1928)","journal-title":"Norsk Matematisk Tidsskrift"},{"key":"42_CR21","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404\u2013415. ACM (2006)","DOI":"10.1145\/1168918.1168907"},{"key":"42_CR22","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL, pp. 313\u2013326. ACM (2010)","DOI":"10.1145\/1707801.1706337"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_42","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T13:28:16Z","timestamp":1748698096000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}