{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T07:11:31Z","timestamp":1794381091488,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540227915","type":"print"},{"value":"9783540278641","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27864-1_24","type":"book-chapter","created":{"date-parts":[[2010,9,16]],"date-time":"2010-09-16T12:35:37Z","timestamp":1284640537000},"page":"328-343","source":"Crossref","is-referenced-by-count":3,"title":["Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions"],"prefix":"10.1007","author":[{"given":"Sumit","family":"Gulwani","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"George C.","family":"Necula","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"24_CR1","first-page":"1","volume-title":"15th 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: 15th Annual ACM Symposium on POPL, pp. 1\u201311. ACM, New York (1988)"},{"key":"24_CR2","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1109\/LICS.1997.614938","volume-title":"12th Annual IEEE Symposium on Logic in Computer Science","author":"H. Andersen","year":"1997","unstructured":"Andersen, H., Hulgaard, H.: Boolean expression diagrams. In: 12th Annual IEEE Symposium on Logic in Computer Science, June 1997, pp. 88\u201398. IEEE, Los Alamitos (1997)"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Bahar, R., Frohm, E., Gaona, C., Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Algebraic Decision Diagrams and Their Applications. In: IEEE \/ACM International Conference on CAD, November 1993, pp. 188\u2013191. ACM\/IEEE (1993)","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"24_CR4","volume-title":"Proceedings of the ACM SIGPLAN 2000 Conference on PLDI","author":"T. Ball","year":"2001","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proceedings of the ACM SIGPLAN 2000 Conference on PLDI, May 2001, ACM, New York (2001)"},{"key":"24_CR5","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1016\/S0020-0190(80)90078-2","volume":"10","author":"M. Blum","year":"1980","unstructured":"Blum, M., Chandra, A., Wegman, M.: Equivalence of free boolean graphs can be decided probabilistically in polynomial time. Information Processing Letters\u00a010, 80\u201382 (1980)","journal-title":"Information Processing Letters"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Bryant, R., Chen, Y.: Verification of Arithmetic Circuits with Binary Moment Diagrams. In: 32nd ACM\/IEEE Design Automation Conference (June 1995)","DOI":"10.1145\/217474.217583"},{"key":"24_CR7","first-page":"236","volume-title":"International Conference on Computer Aided Design","author":"R.E. Bryant","year":"1995","unstructured":"Bryant, R.E.: Binary decision diagrams and beyond: Enabling technologies for formal verification. In: International Conference on Computer Aided Design, November 1995, pp. 236\u2013245. IEEE Computer Society Press, Los Alamitos (1995)"},{"key":"24_CR8","first-page":"159","volume-title":"International Conference on Computer Aided Design","author":"E.M. Clarke","year":"1995","unstructured":"Clarke, E.M., Fujita, M., Zhao, X.: Hybrid decision diagrams overcoming the limitations of MTBDDs and BMDs. In: International Conference on Computer Aided Design, November 1995, pp. 159\u2013163. IEEE Computer Society Press, Los Alamitos (1995)"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., McMillan, K.L., Znao, X., Fujiia, M., Yang, J.: Spectral transforms for large boolean functions with applications to technology mapping. In: Proceedings of the 30th ACM\/IEEE Design Automation Conference, June 1993, pp. 54\u201360 (1993)","DOI":"10.1145\/157485.164569"},{"issue":"1","key":"24_CR10","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008663530211","volume":"10","author":"F. Corella","year":"1997","unstructured":"Corella, F., Zhou, Z., Song, X., Langevin, M., Cerny, E.: Multiway decision graphs for automated hardware verification. Formal Methods in System Design: An International Journal\u00a010(1), 7\u201346 (1997)","journal-title":"Formal Methods in System Design: An International Journal"},{"key":"24_CR11","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":"24_CR12","first-page":"627","volume-title":"Proceedings of the Fourteenth Conference on Innovative Applications of Artificial Intelligence","author":"A. Darwiche","year":"2002","unstructured":"Darwiche, A.: A compiler for deterministic decomposable negation normal form. In: Proceedings of the Fourteenth Conference on Innovative Applications of Artificial Intelligence, July 2002, pp. 627\u2013634. AAAI Press, Menlo Park (2002)"},{"key":"24_CR13","unstructured":"Darwiche, A., Huang, J.: Testing equivalence probabilistically. Technical Report D-23, Computer Science Department, UCLA (June 2002)"},{"issue":"8","key":"24_CR14","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Fujita, M., McGeer, P.C.: Introduction to the special issue on multi-terminal binary decision diagrams. Formal Methods in System Design 10(2\/3) (April 1997)","DOI":"10.1023\/A:1008658421514"},{"key":"24_CR16","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1145\/512529.512536","volume-title":"Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation","author":"K. Gargi","year":"2002","unstructured":"Gargi, K.: A sparse algorithm for predicated global value numbering. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, June 17-19, vol.\u00a037(5), pp. 45\u201356. ACM Press, New York (2002)"},{"issue":"10","key":"24_CR17","doi-asserted-by":"publisher","first-page":"1197","DOI":"10.1109\/12.324545","volume":"43","author":"J. Gergov","year":"1994","unstructured":"Gergov, J., Meinel, C.: Efficient boolean manipulation with OBDDs can be extended to FBDDs. IEEE Trans. on Computers\u00a043(10), 1197\u20131209 (1994)","journal-title":"IEEE Trans. on Computers"},{"key":"24_CR18","volume-title":"30th Annual ACM Symposium on POPL","author":"S. Gulwani","year":"2003","unstructured":"Gulwani, S., Necula, G.C.: Discovering affine equalities using random interpretation. In: 30th Annual ACM Symposium on POPL, January 2003, ACM, New York (2003)"},{"key":"24_CR19","volume-title":"31st Annual ACM Symposium on POPL","author":"S. Gulwani","year":"2004","unstructured":"Gulwani, S., Necula, G.C.: Global value numbering using random interpretation. In: 31st Annual ACM Symposium on POPL, January 2004, ACM, New York (2004)"},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Necula, G.C.: Path-sensitive analysis for linear arithmetic and uninterpreted functions. Technical Report UCB\/\/CSD-04-1325, UC-Berkeley (2004)","DOI":"10.1007\/978-3-540-27864-1_24"},{"key":"24_CR21","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":"24_CR22","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":"24_CR23","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511814075","volume-title":"Randomized Algorithms","author":"R. Motwani","year":"1995","unstructured":"Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (1995)"},{"key":"24_CR24","first-page":"83","volume-title":"Proceedings of the ACM SIGPLAN \u201900 Conference on PLDI","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: Proceedings of the ACM SIGPLAN \u201900 Conference on PLDI, June 2000, pp. 83\u201394. ACM, New York (2000)"},{"key":"24_CR25","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/73560.73562","volume-title":"15th Annual ACM Symposium on Principles of Programming Languages","author":"B.K. Rosen","year":"1988","unstructured":"Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: 15th Annual ACM Symposium on Principles of Programming Languages, pp. 12\u201327. ACM, New York (1988)"},{"key":"24_CR26","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)"},{"issue":"4","key":"24_CR27","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1145\/322217.322225","volume":"27","author":"J.T. Schwartz","year":"1980","unstructured":"Schwartz, J.T.: Fast probabilistic algorithms for verification of polynomial identities. JACM\u00a027(4), 701\u2013717 (1980)","journal-title":"JACM"},{"key":"24_CR28","volume-title":"21st Annual ACM Symposium on POPL","author":"D. Weise","year":"1994","unstructured":"Weise, D., Crew, R.F., Ernst, M., Steensgaard, B.: Value dependence graphs: representation without taxation. In: 21st Annual ACM Symposium on POPL, January 1994, ACM, New York (1994)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27864-1_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:24:43Z","timestamp":1605741883000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27864-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540227915","9783540278641"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27864-1_24","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/b99688","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}