{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,21]],"date-time":"2026-09-21T05:19:43Z","timestamp":1789967983249,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642331244","type":"print"},{"value":"9783642331251","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33125-1_10","type":"book-chapter","created":{"date-parts":[[2012,8,29]],"date-time":"2012-08-29T06:47:24Z","timestamp":1346222844000},"page":"111-128","source":"Crossref","is-referenced-by-count":32,"title":["Bilateral Algorithms for Symbolic Abstraction"],"prefix":"10.1007","author":[{"given":"Aditya","family":"Thakur","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matt","family":"Elder","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"10_CR1","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)"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Barrett, E., King, A.: Range and set abstraction using SAT. ENTCS 267(1) (2010)","DOI":"10.1016\/j.entcs.2010.09.003"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-15769-1_11","volume-title":"Static Analysis","author":"J. Brauer","year":"2010","unstructured":"Brauer, J., King, A.: Automatic Abstraction for Intervals Using Boolean Formulae. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 167\u2013183. Springer, Heidelberg (2010)"},{"key":"10_CR4","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":"10_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Mauborgne, L.: Logical abstract domains and interpretations. In: The Future of Software Engineering (2011)","DOI":"10.1007\/978-3-642-15187-3_3"},{"key":"10_CR7","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":"10_CR8","doi-asserted-by":"crossref","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Sym. Logic\u00a022(3) (September 1957)","DOI":"10.2307\/2963594"},{"key":"10_CR9","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":"10_CR10","unstructured":"Dutertre, B., de Moura, L.: Yices: An SMT solver (2006), yices.csl.sri.com\/"},{"key":"10_CR11","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":"10_CR12","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)"},{"key":"10_CR13","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: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 193\u2013207. Springer, Heidelberg (2008)"},{"key":"10_CR14","unstructured":"Kidd, N., Lal, A., Reps, T.: WALi: The Weighted Automaton Library (2007), http:\/\/www.cs.wisc.edu\/wpis\/wpds\/download.php"},{"key":"10_CR15","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":"10_CR16","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":"10_CR17","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":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-19129-1_4","volume-title":"Foundations of Logic and Functional Programming","author":"J.-L. Lassez","year":"1988","unstructured":"Lassez, J.-L., Maher, M.J., Marriott, K.: Unification Revisited. In: Boscarol, M., Carlucci Aiello, L., Levi, G. (eds.) Foundations of Logic and Functional Programming. LNCS, vol.\u00a0306, pp. 67\u2013113. Springer, Heidelberg (1988)"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-540-78791-4_3","volume-title":"Compiler Construction","author":"J. Lim","year":"2008","unstructured":"Lim, J., Reps, T.: A System for Generating Static Analyzers for Machine Instructions. In: Hendren, L. (ed.) CC 2008. LNCS, vol.\u00a04959, pp. 36\u201352. Springer, Heidelberg (2008)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: WCRE, pp. 310\u2013322 (2001)","DOI":"10.1109\/WCRE.2001.957836"},{"key":"10_CR21","volume-title":"Machine Learning","author":"T. Mitchell","year":"1997","unstructured":"Mitchell, T.: Machine Learning. WCB\/McGraw-Hill, Boston (1997)"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: Automatic modular abstractions for template numerical constraints. Logical Methods in Comp. Sci.\u00a06(3) (2010)","DOI":"10.2168\/LMCS-6(3:4)2010"},{"key":"10_CR23","unstructured":"Plotkin, G.: A note on inductive generalization. In: Machine Intelligence, vol.\u00a05, pp. 153\u2013165. Edinburgh Univ. Press (1970)"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Regehr, J., Reid, A.: HOIST: A system for automatically deriving static analyzers for embedded systems. In: ASPLOS (2004)","DOI":"10.1145\/1024393.1024410"},{"key":"10_CR25","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":"1","key":"10_CR26","first-page":"135","volume":"5","author":"J. Reynolds","year":"1970","unstructured":"Reynolds, J.: Transformational systems and the algebraic structure of atomic formulas. Machine Intelligence\u00a05(1), 135\u2013151 (1970)","journal-title":"Machine Intelligence"},{"issue":"3","key":"10_CR27","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":"10_CR28","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)"},{"issue":"1","key":"10_CR29","first-page":"23","volume":"16","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. FMSD\u00a016(1), 23\u201358 (2000)","journal-title":"FMSD"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Steffen, B., Knoop, J., R\u00fcthing, O.: The value flow graph: A program representation for optimal program transformations. In: ESOP (1990)","DOI":"10.1007\/3-540-52592-0_76"},{"key":"10_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/3540539816_78","volume-title":"TAPSOFT \u201991. Proceedings of the International Joint Conference on Theory and Practice of Software Development, Brighton, UK, April 8-12, 1991","author":"B. Steffen","year":"1991","unstructured":"Steffen, B., Knoop, J., R\u00fcthing, O.: Efficient Code Motion and an Adaption to Strength Reduction. In: Abramsky, S., Maibaum, T.S.E. (eds.) TAPSOFT 1991, CCPSD 1991, and ADC-Talks 1991. LNCS, vol.\u00a0494, pp. 394\u2013415. Springer, Heidelberg (1991)"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Thakur, A., Elder, M., Reps, T.: Bilateral algorithms for symbolic abstraction. TR 1713, CS Dept., Univ. of Wisconsin, Madison, WI (March 2012), http:\/\/www.cs.wisc.edu\/wpis\/papers\/tr1713.pdf","DOI":"10.1007\/978-3-642-33125-1_10"},{"key":"10_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-642-33125-1_23","volume-title":"SAS 2012","author":"A. Thakur","year":"2012","unstructured":"Thakur, A., Reps, T.: A Generalization of St\u00e5lmarck\u2019s Method. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 334\u2013351. Springer, Heidelberg (2012)"},{"key":"10_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-31424-7_17","volume-title":"Computer Aided Verification","author":"A. Thakur","year":"2012","unstructured":"Thakur, A., Reps, T.: A Method for Symbolic Computation of Abstract Operations. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 174\u2013192. Springer, Heidelberg (2012)"},{"key":"10_CR35","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","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33125-1_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T12:16:46Z","timestamp":1744028206000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33125-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642331244","9783642331251"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33125-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}