{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T21:03:00Z","timestamp":1791061380477,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642314230","type":"print"},{"value":"9783642314247","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_17","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T10:26:49Z","timestamp":1340274409000},"page":"174-192","source":"Crossref","is-referenced-by-count":48,"title":["A Method for Symbolic Computation of Abstract Operations"],"prefix":"10.1007","author":[{"given":"Aditya","family":"Thakur","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/10720246_8","volume-title":"Recent Advances in AI Planning","author":"A. Armando","year":"2000","unstructured":"Armando, A., Castellini, C., Giunchiglia, E.: SAT-Based Procedures for Temporal Reasoning. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol.\u00a01809, pp. 97\u2013108. Springer, Heidelberg (2000)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/3-540-45319-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2001","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian Abstraction for Model Checking C Programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 268\u2013283. Springer, Heidelberg (2001)"},{"issue":"1","key":"17_CR3","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/s10817-008-9115-4","volume":"42","author":"M. Bj\u00f6rk","year":"2009","unstructured":"Bj\u00f6rk, M.: First order St\u00e5lmarck. J. Autom. Reasoning\u00a042(1), 99\u2013122 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"17_CR4","unstructured":"Bj\u00f8rner, N., de Moura, L.: Accelerated lemma learning using joins\u2013DPLL(\u2294). In: LPAR (2008)"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Velev, M.N.: Boolean satisfiability with transitivity constraints. Trans. on Computational Logic\u00a03(4) (2002)","DOI":"10.1145\/566385.566390"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. FMSD\u00a025(2-3) (2004)","DOI":"10.1023\/B:FORM.0000040025.89719.f3"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL (1979)","DOI":"10.1145\/567752.567778"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear constraints among variables of a program. In: POPL (1978)","DOI":"10.1145\/512760.512770"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM\u00a05(7) (1962)","DOI":"10.1145\/368273.368557"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM\u00a07(3) (1960)","DOI":"10.1145\/321033.321034"},{"key":"17_CR11","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":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-642-23702-7_17","volume-title":"Static Analysis","author":"M. Elder","year":"2011","unstructured":"Elder, M., Lim, J., Sharma, T., Andersen, T., Reps, T.: Abstract Domains of Affine Relations. In: Yahav, E. (ed.) SAS 2011. LNCS, vol.\u00a06887, pp. 198\u2013215. Springer, Heidelberg (2011)"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-45069-6_34","volume-title":"Computer Aided Verification","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem Proving Using Lazy Proof Explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 355\u2013367. Springer, Heidelberg (2003)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"1","key":"17_CR15","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1145\/321921.321939","volume":"23","author":"S. Graham","year":"1976","unstructured":"Graham, S., Wegman, M.: A fast and usually linear algorithm for data flow analysis. J. ACM\u00a023(1), 172\u2013202 (1976)","journal-title":"J. ACM"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-56287-7_95","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"P. Granger","year":"1992","unstructured":"Granger, P.: Improving the Results of Static Analyses Programs by Local Decreasing Iteration. In: Shyamasundar, R.K. (ed.) FSTTCS 1992. LNCS, vol.\u00a0652, pp. 68\u201379. Springer, Heidelberg (1992)"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-78739-6_16","volume-title":"Programming Languages and Systems","author":"S. Gulwani","year":"2008","unstructured":"Gulwani, S., Musuvathi, M.: Cover Algorithms and Their Combination. In: Gairing, M. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 193\u2013207. Springer, Heidelberg (2008)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/BFb0105407","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: St\u00e5lmarck\u2019s Algorithm as a HOL Derived Rule. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 221\u2013234. Springer, Heidelberg (1996)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Karr, M.: Affine relationship among variables of a program. Acta Inf.\u00a06 (1976)","DOI":"10.1007\/BF00268497"},{"key":"17_CR20","unstructured":"Kidd, N., Lal, A., Reps, T.: WALi: The Weighted Automaton Library (2007), www.cs.wisc.edu\/wpis\/wpds\/download.php"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-11319-2_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. King","year":"2010","unstructured":"King, A., S\u00f8ndergaard, H.: Automatic Abstraction for Congruences. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 197\u2013213. Springer, Heidelberg (2010)"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/3-540-55984-1_13","volume-title":"Compiler Construction","author":"J. Knoop","year":"1992","unstructured":"Knoop, J., Steffen, B.: Interprocedural Coincidence Theorem. In: Pfahler, P., Kastens, U. (eds.) CC 1992. LNCS, vol.\u00a0641, pp. 125\u2013140. Springer, Heidelberg (1992)"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/11817963_32","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2006","unstructured":"Lal, A., Reps, T.: Improving Pushdown System Model Checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 343\u2013357. Springer, Heidelberg (2006)"},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/11513988_44","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2005","unstructured":"Lal, A., Reps, T., Balakrishnan, G.: Extended Weighted Pushdown Systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 434\u2013448. Springer, Heidelberg (2005)"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-642-02658-4_35","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2009","unstructured":"McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to Richer Logics. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 462\u2013476. Springer, Heidelberg (2009)"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: Automatic modular abstractions for template numerical constraints. LMCS\u00a06(3) (2010)","DOI":"10.2168\/LMCS-6(3:4)2010"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Analysis of modular arithmetic. TOPLAS (2007)","DOI":"10.1145\/1275497.1275504"},{"key":"17_CR28","unstructured":"PPL: The Parma polyhedra library, http:\/\/www.cs.unipr.it\/ppl\/"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic Implementation of the Best Transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"issue":"3","key":"17_CR30","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS\u00a024(3), 217\u2013298 (2002)","journal-title":"TOPLAS"},{"key":"17_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-30579-8_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable Analysis of Linear Systems Using Mathematical Programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 25\u201341. Springer, Heidelberg (2005)"},{"key":"17_CR32","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications. Prentice-Hall (1981)"},{"key":"17_CR33","doi-asserted-by":"crossref","unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. FMSD\u00a016(1) (2000)","DOI":"10.1023\/A:1008725524946"},{"key":"17_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-36126-X_10","volume-title":"Formal Methods in Computer-Aided Design","author":"O. Strichman","year":"2002","unstructured":"Strichman, O.: On Solving Presburger and Linear Arithmetic with SAT. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 160\u2013170. Springer, Heidelberg (2002)"},{"key":"17_CR35","unstructured":"Thakur, A., Reps, T.: A generalization of St\u00e5lmarck\u2019s method. TR 1699. CS Dept., Univ. of Wisconsin, Madison, WI (October 2011)"},{"key":"17_CR36","doi-asserted-by":"crossref","unstructured":"Thakur, A., Reps, T.: A method for symbolic computation of precise abstract operations. TR 1708. CS Dept., Univ. of Wisconsin, Madison, WI (January 2012)","DOI":"10.1007\/978-3-642-31424-7_17"},{"key":"17_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-540-24730-2_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Yorsh","year":"2004","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 530\u2013545. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,19]],"date-time":"2022-01-19T01:15:18Z","timestamp":1642554918000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}