{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:28:39Z","timestamp":1767929319326,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642157684","type":"print"},{"value":"9783642157691","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15769-1_15","type":"book-chapter","created":{"date-parts":[[2010,9,13]],"date-time":"2010-09-13T06:09:40Z","timestamp":1284358180000},"page":"236-252","source":"Crossref","is-referenced-by-count":19,"title":["Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis"],"prefix":"10.1007","author":[{"given":"Isil","family":"Dillig","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Dillig","sequence":"additional","affiliation":[]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Een","year":"2005","unstructured":"Een, N., Sorensson, N.: MiniSat: A SAT solver with conflict-clause minimization. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, Springer, Heidelberg (2005)"},{"key":"15_CR2","unstructured":"Kim, J., Silva, J., Savoj, H., Sakallah, K.: RID-GRASP: Redundancy identification and removal using GRASP. In: International Workshop on Logic Synthesis (1997)"},{"key":"15_CR3","first-page":"530","volume-title":"DAC","author":"S. Malik","year":"2001","unstructured":"Malik, S., Zhao, Y., Madigan, C., Zhang, L., Moskewicz, M.: Chaff: Engineering an Efficient SAT Solver. In: DAC, pp. 530\u2013535. ACM, New York (2001)"},{"key":"15_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.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"15_CR5","unstructured":"Dutertre, B., De Moura, L.: The Yices SMT Solver. Technical report, SRI (2006)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2008","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 299\u2013303. Springer, Heidelberg (2008)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-70545-1_27","volume-title":"Computer Aided Verification","author":"M. Bofill","year":"2008","unstructured":"Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodr\u0131guez-Carbonell, E., Rubio, A.: The Barcelogic SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, p. 294. Springer, Heidelberg (2008)"},{"issue":"5","key":"15_CR9","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. JACM\u00a050(5), 752\u2013794 (2003)","journal-title":"JACM"},{"key":"15_CR10","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"POPL","author":"T. Henzinger","year":"2002","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370. ACM, New York (2002)"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.: The SLAM project: debugging system software via static analysis. In: POPL, NY, USA, pp.1\u20133 (2002)","DOI":"10.1145\/503272.503274"},{"issue":"5","key":"15_CR12","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1145\/543552.512538","volume":"37","author":"M. Das","year":"2002","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. ACM SIGPLAN Notices\u00a037(5), 57\u201368 (2002)","journal-title":"ACM SIGPLAN Notices"},{"key":"15_CR13","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1145\/1040305.1040334","volume-title":"POPL","author":"Y. Xie","year":"2005","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: POPL, vol.\u00a040, pp. 351\u2013363. ACM, New York (2005)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Bugrara, S., Aiken, A.: Verifying the safety of user pointer dereferences. In: IEEE Symposium on Security and Privacy, SP 2008, pp. 325\u2013338 (2008)","DOI":"10.1109\/SP.2008.15"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/3-540-60609-2_25","volume-title":"Fundamentals of Contex-Sensitive Rewriting","author":"S. Lucas","year":"1995","unstructured":"Lucas, S.: Fundamentals of Contex-Sensitive Rewriting. LNCS, pp. 405\u2013412. Springer, Heidelberg (1995)"},{"issue":"1","key":"15_CR16","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1016\/S0747-7171(03)00025-7","volume":"36","author":"A. Armando","year":"2003","unstructured":"Armando, A., Ranise, S.: Constraint contextual rewriting. Journal of Symbolic Computation\u00a036(1), 193\u2013216 (2003)","journal-title":"Journal of Symbolic Computation"},{"issue":"6","key":"15_CR17","doi-asserted-by":"publisher","first-page":"977","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL (T). Journal of the ACM (JACM)\u00a053(6), 977 (2006)","journal-title":"Journal of the ACM (JACM)"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-02658-4_20","volume-title":"Computer Aided Verification","author":"I. Dillig","year":"2009","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: A complete and practical technique for solving linear inequalities over integers. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 233\u2013247. Springer, Heidelberg (2009)"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-11957-6_14","volume-title":"Programming Languages and Systems","author":"I. Dillig","year":"2010","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Fluid Updates: Beyond Strong vs. Weak Updates. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 246\u2013266. Springer, Heidelberg (2010)"},{"key":"15_CR20","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1145\/1368088.1368118","volume-title":"ICSE","author":"D. Babi\u0107","year":"2008","unstructured":"Babi\u0107, D., Hu, A.J.: Calysto: Scalable and Precise Extended Static Checking. In: ICSE, pp. 211\u2013220. ACM, New York (May 2008)"},{"key":"15_CR21","first-page":"96","volume-title":"PLDI","author":"M. Faehndrich","year":"1998","unstructured":"Faehndrich, M., Foster, J., Su, Z., Aiken, A.: Partial online cycle elimination in inclusion constraint graphs. In: PLDI, p. 96. ACM, New York (1998)"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.: DAG-aware AIG rewriting: A fresh look at combinational logic synthesis. In: DAC, pp.532\u2013535 (2006)","DOI":"10.1145\/1146909.1147048"},{"key":"15_CR23","unstructured":"Mishchenko, A., Brayton, R., Jiang, J., Jang, S.: SAT-based logic optimization and resynthesis. In: Proc. IWLS 2007, pp. 358\u2013364 (2007)"},{"issue":"2","key":"15_CR24","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O. Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.: Vacuity detection in temporal model checking. International Journal on Software Tools for Technology Transfer\u00a04(2), 224\u2013233 (2003)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1007\/978-3-540-45069-6_35","volume-title":"Enhanced vacuity detection in linear temporal logic","author":"R. Armoni","year":"2003","unstructured":"Armoni, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A., Vardi, M.: Enhanced vacuity detection in linear temporal logic. LNCS, pp. 368\u2013380. Springer, Heidelberg (2003)"},{"issue":"3","key":"15_CR26","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. Bryant","year":"1992","unstructured":"Bryant, R.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys (CSUR)\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Computing Surveys (CSUR)"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Bryant, R., Chen, Y.: Verification of arithmetic functions with BMDs (1994)","DOI":"10.21236\/ADA281028"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Clarke, E., Fujita, M., Zhao, X.: Hybrid decision diagrams overcoming the limitations of MTBDDs and BMDs. In: ICCAD (1995)","DOI":"10.21236\/ADA296684"},{"key":"15_CR29","unstructured":"Cheng, K., Yap, R.: Constrained decision diagrams. In: Proceedings of the National Conference on Artificial Intelligence, vol.\u00a020, p. 366 (2005)"},{"key":"15_CR30","first-page":"97","volume-title":"Proc. 5th Conf. on Automated Deduction (CADE)","author":"D. Loveland","year":"1987","unstructured":"Loveland, D., Shostak, R.: Simplifying interpreted formulas. In: Proc. 5th Conf. on Automated Deduction (CADE), vol.\u00a087, pp. 97\u2013109. Springer, Heidelberg (1987)"},{"key":"15_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V. Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, p. 519. Springer, Heidelberg (2007)"},{"key":"15_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1007\/978-3-642-02658-4_53","volume-title":"Computer Aided Verification","author":"S. Jha","year":"2009","unstructured":"Jha, S., Limaye, R., Seshia, S.: Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 668\u2013674. Springer, Heidelberg (2009)"},{"issue":"6","key":"15_CR33","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1145\/1543135.1542517","volume":"44","author":"S. Chandra","year":"2009","unstructured":"Chandra, S., Fink, S.J., Sridharan, M.: Snugglebug: a powerful approach to weakest preconditions. SIGPLAN Not.\u00a044(6), 363\u2013374 (2009)","journal-title":"SIGPLAN Not."},{"key":"15_CR34","first-page":"37","volume-title":"Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming","author":"A. Kelly","year":"1996","unstructured":"Kelly, A., Marriott, A., Stuckey, P., Yap, R.: Effectiveness of Optimizing Compilation for CLP (R). In: Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming, p. 37. The MIT Press, Cambridge (1996)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15769-1_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T18:45:13Z","timestamp":1740509113000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15769-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642157684","9783642157691"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15769-1_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}