{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:12:57Z","timestamp":1774987977000,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540240587","type":"print"},{"value":"9783540305385","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30538-5_26","type":"book-chapter","created":{"date-parts":[[2010,3,12]],"date-time":"2010-03-12T13:40:30Z","timestamp":1268401230000},"page":"311-323","source":"Crossref","is-referenced-by-count":15,"title":["Join Algorithms for the Theory of Uninterpreted Functions"],"prefix":"10.1007","author":[{"given":"Sumit","family":"Gulwani","sequence":"first","affiliation":[]},{"given":"Ashish","family":"Tiwari","sequence":"additional","affiliation":[]},{"given":"George C.","family":"Necula","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","first-page":"1","volume-title":"5th Annual ACM Symposium on POPL","author":"B. Alpern","year":"1988","unstructured":"Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In: 5th Annual ACM Symposium on POPL, pp. 1\u201311. ACM, New York (1988)"},{"issue":"2","key":"26_CR2","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1023\/B:JARS.0000009518.26415.49","volume":"31","author":"L. Bachmair","year":"2003","unstructured":"Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. J. of Automated Reasoning\u00a031(2), 129\u2013168 (2003)","journal-title":"J. of Automated Reasoning"},{"key":"26_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: ACM PLDI 2003, pp. 196\u2013207 (2003)","DOI":"10.1145\/781131.781153"},{"issue":"6","key":"26_CR4","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1002\/(SICI)1097-024X(199706)27:6<701::AID-SPE104>3.0.CO;2-0","volume":"27","author":"P. Briggs","year":"1997","unstructured":"Briggs, P., Cooper, K.D., Simpson, L.T.: Value numbering. Software Practice and Experience\u00a027(6), 701\u2013724 (1997)","journal-title":"Software Practice and Experience"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th Annual ACM Symposium on Principles of Programming Languages, pp. 234\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Fifth ACM Symposium on POPL, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"issue":"4","key":"26_CR7","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R. Cytron","year":"1990","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems\u00a013(4), 451\u2013490 (1990)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-540-27864-1_17","volume-title":"Static Analysis","author":"S. Gulwani","year":"2004","unstructured":"Gulwani, S., Necula, G.C.: A polynomial-time algorithm for global value numbering. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 212\u2013227. Springer, Heidelberg (2004)"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/3-540-62950-5_59","volume-title":"Rewriting Techniques and Applications","author":"D. Kapur","year":"1997","unstructured":"Kapur, D.: Shostak\u2019s congruence closure as completion. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol.\u00a01103, pp. 23\u201337. Springer, Heidelberg (1997)"},{"key":"26_CR10","first-page":"133","volume-title":"Acta Informatica","author":"M. Karr","year":"1976","unstructured":"Karr, M.: Affine relationships among variables of a program. In: Acta Informatica, pp. 133\u2013151. Springer, Heidelberg (1976)"},{"key":"#cr-split#-26_CR11.1","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Partial automata and finitely generated congruences: an extension of Nerode\u2019s theorem. In: Shore, R. (ed.) Proc. Conf. Logical Methods in Math. and Comp. Sci. (1992);","DOI":"10.7146\/dpb.v21i400.6634"},{"key":"#cr-split#-26_CR11.2","unstructured":"Also Tech. Rep. PB-400, Comp. Sci. Dept., Aarhus Univ. (1992)"},{"key":"26_CR12","volume-title":"Advanced Compiler Design and Implementation","author":"S.S. Muchnick","year":"2000","unstructured":"Muchnick, S.S.: Advanced Compiler Design and Implementation. Morgan Kaufmann, San Francisco (2000)"},{"key":"26_CR13","first-page":"330","volume-title":"31st ACM Symposium on POPL","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: 31st ACM Symposium on POPL, pp. 330\u2013341. ACM, New York (2004)"},{"issue":"2","key":"26_CR14","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"26_CR15","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.: Fast decision procedures based on congruence closure. Journal of the Association for Computing Machinery\u00a027(2), 356\u2013364 (1980)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"26_CR16","first-page":"49","volume-title":"22nd ACM Symposium on POPL","author":"T. Reps","year":"1995","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: 22nd ACM Symposium on POPL, pp. 49\u201361. ACM, New York (1995)"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-27864-1_21","volume-title":"Static Analysis","author":"E. Rodriguez-Carbonell","year":"2004","unstructured":"Rodriguez-Carbonell, E., Kapur, D.: An abstract interpretation approach for automatic generation of polynomial invariants. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 280\u2013295. Springer, Heidelberg (2004)"},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-48294-6_15","volume-title":"Static Analysis","author":"O. R\u00fcthing","year":"1999","unstructured":"R\u00fcthing, O., Knoop, J., Steffen, B.: Detecting equalities of variables: Combining efficiency with precision. In: Cortesi, A., Fil\u00e9, G. (eds.) SAS 1999. LNCS, vol.\u00a01694, pp. 232\u2013247. Springer, Heidelberg (1999)"},{"key":"26_CR19","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/S0304-3975(02)00080-4","volume":"300","author":"S. Vagvolgyi","year":"2003","unstructured":"Vagvolgyi, S.: Intersection of finitely generated congruences over term algebra. Theoretical Computer Science\u00a0300, 209\u2013234 (2003)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30538-5_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:58:49Z","timestamp":1605761929000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30538-5_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540240587","9783540305385"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30538-5_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}