{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T16:45:21Z","timestamp":1725727521335},"publisher-location":"Berlin, Heidelberg","reference-count":47,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642391750"},{"type":"electronic","value":"9783642391767"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39176-7_18","type":"book-chapter","created":{"date-parts":[[2013,5,30]],"date-time":"2013-05-30T04:58:44Z","timestamp":1369889924000},"page":"282-300","source":"Crossref","is-referenced-by-count":3,"title":["Automatic Equivalence Checking of UF+IA Programs"],"prefix":"10.1007","author":[{"given":"Nuno P.","family":"Lopes","sequence":"first","affiliation":[]},{"given":"Jos\u00e9","family":"Monteiro","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools, 2nd edn. Addison-Wesley (2006)"},{"key":"18_CR2","unstructured":"Alias, C., Barthou, D.: On the recognition of algorithm templates. In: COCV (2003)"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL (2002)","DOI":"10.1145\/503272.503274"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-21437-0_17","volume-title":"FM 2011: Formal Methods","author":"G. Barthe","year":"2011","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 200\u2013214. Springer, Heidelberg (2011)"},{"key":"18_CR5","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: CSFW (2004)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/3-540-45706-2_40","volume-title":"Euro-Par 2002. Parallel Processing","author":"D. Barthou","year":"2002","unstructured":"Barthou, D., Feautrier, P., Redon, X.: On the equivalence of two systems of affine recurrence equations. In: Monien, B., Feldmann, R.L. (eds.) Euro-Par 2002. LNCS, vol.\u00a02400, pp. 309\u2013313. Springer, Heidelberg (2002)"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL (2004)","DOI":"10.1145\/964001.964003"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-69738-1_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 378\u2013394. Springer, Heidelberg (2007)"},{"key":"18_CR9","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":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-17511-4_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Blanc","year":"2010","unstructured":"Blanc, R., Henzinger, T.A., Hottelier, T., Kov\u00e1cs, L.: ABC: Algebraic bound computation for loops. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 103\u2013118. Springer, Heidelberg (2010)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-27940-9_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Chaki","year":"2012","unstructured":"Chaki, S., Gurfinkel, A., Strichman, O.: Regression verification for multi-threaded programs. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 119\u2013135. Springer, Heidelberg (2012)"},{"key":"18_CR12","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.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Godlin, B., Strichman, O.: Regression verification. In: DAC (2009)","DOI":"10.1145\/1629911.1630034"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Goldberg, B., Zuck, L., Barrett, C.: Into the loops: Practical issues in translation validation for optimizing compilers. Electron. Notes Theor. Comp. Sci. 132 (2005)","DOI":"10.1016\/j.entcs.2005.01.030"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012)","DOI":"10.1145\/2254064.2254112"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.: SPEED: precise and efficient static estimation of program computational complexity. In: POPL (2009)","DOI":"10.1145\/1480881.1480898"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/11693024_19","volume-title":"Programming Languages and Systems","author":"S. Gulwani","year":"2006","unstructured":"Gulwani, S., Tiwari, A.: Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol.\u00a03924, pp. 279\u2013293. Springer, Heidelberg (2006)"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Guo, S.-Y., Palsberg, J.: The essence of compiling with traces. In: POPL (2011)","DOI":"10.1145\/1926385.1926450"},{"key":"18_CR19","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":"18_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL (2004)","DOI":"10.1145\/964001.964021"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)","DOI":"10.1145\/503272.503279"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11513988_31","volume-title":"Computer Aided Verification","author":"F. Ivan\u010di\u0107","year":"2005","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: Software verification platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 301\u2013306. Springer, Heidelberg (2005)"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Kundu, S., Tatlock, Z., Lerner, S.: Proving optimizations correct using parameterized program equivalence. In: PLDI (2009)","DOI":"10.1145\/1542476.1542513"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"712","DOI":"10.1007\/978-3-642-31424-7_54","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2012","unstructured":"Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Reb\u00ealo, H.: SymDiff: A language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 712\u2013717. Springer, Heidelberg (2012)"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X., Fu, M.: A rely-guarantee-based simulation for verifying concurrent program transformations. In: POPL (2012)","DOI":"10.1145\/2103656.2103711"},{"key":"18_CR26","unstructured":"Matsumoto, T., Saito, H., Fujita, M.: Equivalence checking of C programs by locally performing symbolic simulation on dependence graphs. In: ISQED (2006)"},{"key":"18_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"18_CR28","unstructured":"McMillan, K.L.: Interpolants from Z3 proofs. In: FMCAD (2011)"},{"key":"18_CR29","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/j.ipl.2004.05.004","volume":"91","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Computing polynomial program invariants. Inf. Process. Lett.\u00a091, 233\u2013244 (2004)","journal-title":"Inf. Process. Lett."},{"key":"18_CR30","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI (2000)","DOI":"10.1145\/349299.349314"},{"key":"18_CR31","doi-asserted-by":"crossref","unstructured":"Person, S., Dwyer, M.B., Elbaum, S., P\u01ces\u01cereanu, C.S.: Differential symbolic execution. In: SIGSOFT (2008)","DOI":"10.1145\/1453101.1453131"},{"key":"18_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"key":"18_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-69611-7_16","volume-title":"Practical Aspects of Declarative Languages","author":"A. Podelski","year":"2007","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 245\u2013259. Springer, Heidelberg (2007)"},{"key":"18_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"669","DOI":"10.1007\/978-3-642-22110-1_55","volume-title":"Computer Aided Verification","author":"D.A. Ramos","year":"2011","unstructured":"Ramos, D.A., Engler, D.R.: Practical, low-effort equivalence verification of real code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 669\u2013685. Springer, Heidelberg (2011)"},{"key":"18_CR35","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1016\/j.jsc.2007.01.002","volume":"42","author":"E. Rodr\u00edguez-Carbonell","year":"2007","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. J. Symb. Comput.\u00a042, 443\u2013476 (2007)","journal-title":"J. Symb. Comput."},{"key":"18_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-69738-1_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Rybalchenko","year":"2007","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 346\u2013362. Springer, Heidelberg (2007)"},{"issue":"4","key":"18_CR37","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1516507.1516510","volume":"31","author":"D. Sangiorgi","year":"2009","unstructured":"Sangiorgi, D.: On the origins of bisimulation and coinduction. ACM Trans. Program. Lang. Syst. 31(4), 15:1\u201315:41 (2009)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"18_CR38","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: POPL (2004)","DOI":"10.1145\/964001.964028"},{"key":"18_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-540-31985-6_15","volume-title":"Compiler Construction","author":"K.C. Shashidhar","year":"2005","unstructured":"Shashidhar, K.C., Bruynooghe, M., Catthoor, F., Janssens, G.: Verification of source code transformations by program equivalence checking. In: Bodik, R. (ed.) CC 2005. LNCS, vol.\u00a03443, pp. 221\u2013236. Springer, Heidelberg (2005)"},{"key":"18_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-642-22110-1_59","volume-title":"Computer Aided Verification","author":"M. Stepp","year":"2011","unstructured":"Stepp, M., Tate, R., Lerner, S.: Equality-based translation validator for LLVM. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 737\u2013742. Springer, Heidelberg (2011)"},{"key":"18_CR41","unstructured":"Strang, G.: Linear Algebra and Its Applications, 2nd edn. Academic Press (1980)"},{"key":"18_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T. Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 352\u2013367. Springer, Heidelberg (2005)"},{"key":"18_CR43","doi-asserted-by":"crossref","unstructured":"Tristan, J.-B., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for LLVM. In: PLDI (2011)","DOI":"10.1145\/1993498.1993533"},{"key":"18_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"599","DOI":"10.1007\/978-3-642-02658-4_44","volume-title":"Computer Aided Verification","author":"S. Verdoolaege","year":"2009","unstructured":"Verdoolaege, S., Janssens, G., Bruynooghe, M.: Equivalence checking of static affine programs using widening to handle recurrences. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 599\u2013613. Springer, Heidelberg (2009)"},{"key":"18_CR45","doi-asserted-by":"crossref","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: PLDI (2011)","DOI":"10.1145\/1993498.1993532"},{"key":"18_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-68237-0_5","volume-title":"FM 2008: Formal Methods","author":"A. Zaks","year":"2008","unstructured":"Zaks, A., Pnueli, A.: CoVaC: Compiler validation by program analysis of the cross-product. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 35\u201351. Springer, Heidelberg (2008)"},{"key":"18_CR47","doi-asserted-by":"crossref","unstructured":"Zuck, L., Pnueli, A., Goldberg, B., Barrett, C., Fang, Y., Hu, Y.: Translation and run-time validation of loop transformations. Form. Methods Syst. Des.\u00a027 (2005)","DOI":"10.1007\/s10703-005-3402-z"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39176-7_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T08:55:54Z","timestamp":1557737754000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39176-7_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642391750","9783642391767"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39176-7_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}