{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:46:29Z","timestamp":1780994789589,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":85,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662491218","type":"print"},{"value":"9783662491225","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,12,25]],"date-time":"2015-12-25T00:00:00Z","timestamp":1451001600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49122-5_1","type":"book-chapter","created":{"date-parts":[[2015,12,24]],"date-time":"2015-12-24T00:01:36Z","timestamp":1450915296000},"page":"3-40","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Automating Abstract Interpretation"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Reps","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aditya","family":"Thakur","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"issue":"4","key":"1_CR1","first-page":"487","volume":"7","author":"S Akers Jr","year":"1959","unstructured":"Akers Jr, S.: On a theory of Boolean functions. J. SIAM 7(4), 487\u2013498 (1959)","journal-title":"J. SIAM"},{"issue":"2","key":"1_CR2","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87\u2013106 (1987)","journal-title":"Inf. Comput."},{"key":"1_CR3","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/S0304-3975(99)00032-8","volume":"221","author":"K Apt","year":"1999","unstructured":"Apt, K.: The essence of constraint propagation. TCS 221, 179\u2013210 (1999)","journal-title":"TCS"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/11609773_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G Arnold","year":"2006","unstructured":"Arnold, G., Manevich, R., Sagiv, M., Shaham, R.: Combining shape analyses by intersecting abstractions. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 33\u201348. Springer, Heidelberg (2006)"},{"issue":"1\u20132","key":"1_CR5","first-page":"3","volume":"72","author":"R Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. SCP 72(1\u20132), 3\u201321 (2008)","journal-title":"SCP"},{"issue":"6","key":"1_CR6","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1145\/1749608.1749612","volume":"32","author":"G Balakrishnan","year":"2010","unstructured":"Balakrishnan, G., Reps, T.: WYSINWYX: what you see is not what you eXecute. TOPLAS 32(6), 202\u2013213 (2010)","journal-title":"TOPLAS"},{"key":"1_CR7","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. 2031, pp. 268\u2013283. Springer, Heidelberg (2001)"},{"issue":"1","key":"1_CR8","first-page":"17","volume":"267","author":"E Barrett","year":"2010","unstructured":"Barrett, E., King, A.: Range and set abstraction using SAT. ENTCS 267(1), 17\u201327 (2010)","journal-title":"ENTCS"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD (2009)","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"1_CR10","unstructured":"Beyer, D., Keremoglu, M., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: FMCAD (2010)"},{"key":"1_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines: A Method for High-Level System Design and Analysis","author":"E Boerger","year":"2003","unstructured":"Boerger, E., Staerk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-540-73368-3_25","volume-title":"Computer Aided Verification","author":"I Bogudlov","year":"2007","unstructured":"Bogudlov, I., Lev-Ami, T., Reps, T., Sagiv, M.: Revamping TVLA: Making parametric shape analysis competitive. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 221\u2013225. Springer, Heidelberg (2007)"},{"key":"1_CR13","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. 6337, pp. 167\u2013183. Springer, Heidelberg (2010)"},{"key":"1_CR14","doi-asserted-by":"publisher","first-page":"775","DOI":"10.1002\/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H","volume":"30","author":"W Bush","year":"2000","unstructured":"Bush, W., Pincus, J., Sielaff, D.: A static analyzer for finding dynamic programming errors. Softw. Pract. Experience 30, 775\u2013802 (2000)","journal-title":"Softw. Pract. Experience"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-540-74061-2_25","volume-title":"Static Analysis","author":"C Calcagno","year":"2007","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Footprint analysis: A shape analysis that discovers preconditions. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 402\u2013418. Springer, Heidelberg (2007)"},{"issue":"2\u20133","key":"1_CR16","first-page":"125","volume":"25","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. FMSD 25(2\u20133), 125\u2013127 (2004)","journal-title":"FMSD"},{"key":"1_CR17","first-page":"243","volume-title":"Lecture Notes in Computer Science","author":"Patrick Cousot","year":"2003","unstructured":"Cousot, P.: Verification by abstract interpretation. In: Verification Theory and Practice (2003)"},{"key":"1_CR18","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: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL (1979)","DOI":"10.1145\/567752.567778"},{"issue":"6","key":"1_CR20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2395116.2395120","volume":"59","author":"Patrick Cousot","year":"2012","unstructured":"Cousot, P., Cousot, R., Mauborgne, L.: Theories, solvers and static analysis by abstract interpretation. J. ACM 59(6), Article No. 31 (2012)","journal-title":"Journal of the ACM"},{"key":"1_CR21","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":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-28869-2_9","volume-title":"Programming Languages and Systems","author":"P Cousot","year":"2012","unstructured":"Cousot, P., Monerau, M.: Probabilistic abstract interpretation. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 169\u2013193. Springer, Heidelberg (2012)"},{"issue":"3","key":"1_CR23","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symbolic Logic 22(3), 269\u2013285 (1957)","journal-title":"J. Symbolic Logic"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"1_CR25","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1006\/inco.1995.1102","volume":"120","author":"G Dong","year":"1995","unstructured":"Dong, G., Su, J.: Incremental and decremental evaluation of transitive closure by first-order queries. Inf. Comp. 120, 101\u2013106 (1995)","journal-title":"Inf. Comp."},{"issue":"1","key":"1_CR26","first-page":"43","volume":"267","author":"M Elder","year":"2010","unstructured":"Elder, M., Gopan, D., Reps, T.: View-augmented abstractions. ENTCS 267(1), 43\u201357 (2010)","journal-title":"ENTCS"},{"issue":"4","key":"1_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2651361","volume":"36","author":"M Elder","year":"2014","unstructured":"Elder, M., Lim, J., Sharma, T., Andersen, T., Reps, T.: Abstract domains of affine relations. TOPLAS 36(4), 1\u201373 (2014)","journal-title":"TOPLAS"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Futamura, Y.: Partial evaluation of computation process - an approach to a compiler-compiler. Higher-Order and Symb. Comp., 12(4) (1999). Reprinted from Systems \n                      \n                        \n                      \n                      $$\\cdot $$\n                     Computers \n                      \n                        \n                      \n                      $$\\cdot $$\n                     Controls 2(5) (1971)","DOI":"10.1023\/A:1010043619517"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/11817963_41","volume-title":"Computer Aided Verification","author":"D Gopan","year":"2006","unstructured":"Gopan, D., Reps, T.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 452\u2013466. Springer, Heidelberg (2006)"},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-540-74061-2_22","volume-title":"Static Analysis","author":"D Gopan","year":"2007","unstructured":"Gopan, D., Reps, T.: Guided static analysis. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 349\u2013365. Springer, Heidelberg (2007)"},{"key":"1_CR31","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"Susanne Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: CAV (1997)"},{"key":"1_CR32","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. 4960, pp. 193\u2013207. Springer, Heidelberg (2008)"},{"key":"1_CR33","volume-title":"Materialized Views: Techniques, Implementations, and Applications","year":"1999","unstructured":"Gupta, A., Mumick, I. (eds.): Materialized Views: Techniques, Implementations, and Applications. The M.I.T. Press, Cambridge, MA (1999)"},{"key":"1_CR34","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The M.I.T. Press, Cambridge (2006)"},{"issue":"2","key":"1_CR35","doi-asserted-by":"publisher","first-page":"5:1","DOI":"10.1145\/1667048.1667050","volume":"32","author":"B Jeannet","year":"2010","unstructured":"Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. TOPLAS 32(2), 5:1\u20135:2 (2010)","journal-title":"TOPLAS"},{"key":"1_CR36","unstructured":"Johnson, S.: YACC: Yet another compiler-compiler. Technical Report Comp. Sci. Tech. Rep. 32, Bell Laboratories (1975)"},{"key":"1_CR37","unstructured":"Jones, N., Gomard, C., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall International (1993)"},{"key":"1_CR38","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M Karr","year":"1976","unstructured":"Karr, M.: Affine relationship among variables of a program. Acta Inf. 6, 133\u2013151 (1976)","journal-title":"Acta Inf."},{"key":"1_CR39","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3897.001.0001","volume-title":"An Introduction to Computational Learning Theory","author":"MJ Kearns","year":"1994","unstructured":"Kearns, M.J., Vazirani, U.V.: An Introduction to Computational Learning Theory. MIT Press, Cambridge, MA, USA (1994)"},{"key":"1_CR40","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. 5944, pp. 197\u2013213. Springer, Heidelberg (2010)"},{"issue":"3","key":"1_CR41","first-page":"328","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. JCSS 22(3), 328\u2013350 (1981)","journal-title":"JCSS"},{"key":"1_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis","author":"T Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) Static Analysis. LNCS, vol. 1824, pp. 280\u2013301. Springer, Heidelberg (2000)"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with smt solvers. In: POPL (2014)","DOI":"10.1145\/2535838.2535857"},{"issue":"1","key":"1_CR44","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10009-010-0158-6","volume":"13","author":"J Lim","year":"2011","unstructured":"Lim, J., Lal, A., Reps, T.: Symbolic analysis via semantic reinterpretation. STTT 13(1), 61\u201387 (2011)","journal-title":"STTT"},{"issue":"1","key":"1_CR45","first-page":"1","volume":"35","author":"Junghee Lim","year":"2013","unstructured":"Lim, J., Reps, T.: TSL: A system for generating abstract interpreters and its application to machine-code analysis. In: TOPLAS, 35(1), (2013). Article 4","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR46","unstructured":"Malmkj\u00e6r, K.: Abstract Interpretation of Partial-Evaluation Algorithms. Ph.D. thesis, Dept. of Comp. and Inf. Sci., Kansas State Univ. (1993)"},{"key":"1_CR47","unstructured":"McMillan, K.: Don\u2019t-care computation using k-clause approximation. In: IWLS (2005)"},{"key":"1_CR48","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: WCRE (2001)"},{"key":"1_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-45789-5_11","volume-title":"Static Analysis","author":"A Min\u00e9","year":"2002","unstructured":"Min\u00e9, A.: A few graph-based relational numerical abstract domains. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 117\u2013132. Springer, Heidelberg (2002)"},{"key":"1_CR50","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A., Breck, J., Reps, T.: An algorithm inspired by constraint solvers to infer inductive invariants in numeric programs. Submitted for publication (2015)","DOI":"10.1007\/978-3-662-49498-1_22"},{"key":"1_CR51","volume-title":"Machine Learning","author":"T Mitchell","year":"1997","unstructured":"Mitchell, T.: Machine Learning. WCB\/McGraw-Hill, Boston, MA (1997)"},{"key":"1_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-540-45099-3_17","volume-title":"Static Analysis","author":"D Monniaux","year":"2000","unstructured":"Monniaux, D.: Abstract interpretation of probabilistic semantics. In: Palsberg, J. (ed.) Static Analysis. LNCS, vol. 1824, pp. 322\u2013339. Springer, Heidelberg (2000)"},{"issue":"3","key":"1_CR53","first-page":"4","volume":"6","author":"D Monniaux","year":"2010","unstructured":"Monniaux, D.: Automatic modular abstractions for template numerical constraints. LMCS 6(3), 4 (2010)","journal-title":"LMCS"},{"issue":"2","key":"1_CR54","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0020-0255(74)90008-5","volume":"7","author":"U Montanari","year":"1974","unstructured":"Montanari, U.: Networks of constraints: Fundamental properties and applications to picture processing. Inf. Sci. 7(2), 95\u2013132 (1974)","journal-title":"Inf. Sci."},{"issue":"1","key":"1_CR55","doi-asserted-by":"crossref","first-page":"330","DOI":"10.1145\/982962.964029","volume":"39","author":"Markus M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL (2004)","journal-title":"ACM SIGPLAN Notices"},{"key":"1_CR56","doi-asserted-by":"crossref","unstructured":"Mycroft, A., Jones, N.: A relational framework for abstract interpretation. In: Programs as Data Objects (1985)","DOI":"10.1007\/3-540-16446-4_9"},{"key":"1_CR57","unstructured":"Mycroft, A., Jones, N.: Data flow analysis of applicative programs using minimal function graphs. In: POPL (1986)"},{"key":"1_CR58","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0304-3975(89)90091-1","volume":"69","author":"F Nielson","year":"1989","unstructured":"Nielson, F.: Two-level semantics and abstract interpretation. TCS 69, 117\u2013242 (1989)","journal-title":"TCS"},{"issue":"2","key":"1_CR59","first-page":"199","volume":"55","author":"S Patnaik","year":"1997","unstructured":"Patnaik, S., Immerman, N.: Dyn-FO: A parallel, dynamic complexity class. JCSS 55(2), 199\u2013209 (1997)","journal-title":"JCSS"},{"key":"1_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-642-35873-9_26","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Pelleau","year":"2013","unstructured":"Pelleau, M., Min\u00e9, A., Truchet, C., Benhamou, F.: A constraint solver based on abstract domains. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 434\u2013454. Springer, Heidelberg (2013)"},{"key":"1_CR61","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":"1_CR62","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL (1995)","DOI":"10.1145\/199448.199462"},{"issue":"32","key":"1_CR63","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1749608.1749613","volume":"6","author":"T Reps","year":"2010","unstructured":"Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. TOPLAS 6(32), 1\u201355 (2010)","journal-title":"TOPLAS"},{"key":"1_CR64","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. 2937, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"issue":"1\u20132","key":"1_CR65","first-page":"206","volume":"58","author":"T Reps","year":"2005","unstructured":"Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. SCP 58(1\u20132), 206\u2013263 (2005)","journal-title":"SCP"},{"key":"1_CR66","unstructured":"Reps, T., Thakur, A.: Through the lens of abstraction. In: HCSS (2014)"},{"issue":"1","key":"1_CR67","doi-asserted-by":"crossref","first-page":"663","DOI":"10.1145\/2914770.2837659","volume":"51","author":"Thomas Reps","year":"2016","unstructured":"Reps, T., Turetsky, E., Prabhu, P.: Newtonian program analysis via tensor product. In: POPL (2016)","journal-title":"ACM SIGPLAN Notices"},{"key":"1_CR68","unstructured":"Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)"},{"issue":"1","key":"1_CR69","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"M Sagiv","year":"1998","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. TOPLAS 20(1), 1\u201350 (1998)","journal-title":"TOPLAS"},{"issue":"3","key":"1_CR70","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 24(3), 217\u2013298 (2002)","journal-title":"TOPLAS"},{"key":"1_CR71","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. 3385, pp. 25\u201341. Springer, Heidelberg (2005)"},{"key":"1_CR72","doi-asserted-by":"crossref","unstructured":"Scherpelz, E., Lerner, S., Chambers, C.: Automatic inference of optimizer flow functions from semantic meanings. In: PLDI (2007)","DOI":"10.1145\/1250734.1250750"},{"issue":"2","key":"1_CR73","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1145\/357162.357166","volume":"4","author":"M Sharir","year":"1982","unstructured":"Sharir, M.: Some observations concerning formal differentiation of set theoretic expressions. TOPLAS 4(2), 196\u2013225 (1982)","journal-title":"TOPLAS"},{"key":"1_CR74","series-title":"Program Flow Analysis Theory and Applications","volume-title":"Two approaches to interprocedural data flow analysis","author":"M Sharir","year":"1981","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. Program Flow Analysis Theory and Applications. Prentice-Hall, Englewood Cliffs (1981)"},{"issue":"1","key":"1_CR75","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1023\/A:1008725524946","volume":"16","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. Formal Methods Syst. Des. 16(1), 23\u201358 (2000)","journal-title":"Formal Methods Syst. Des."},{"key":"1_CR76","unstructured":"Thakur, A.: Symbolic Abstraction: Algorithms and Applications. Ph.D. thesis, Comp. Sci. Dept., Univ. of Wisconsin, Madison, WI, Aug. 2014. Technical Report (1812)"},{"key":"1_CR77","doi-asserted-by":"crossref","unstructured":"Thakur, A., Breck, J., Reps, T.: Satisfiability modulo abstraction for separation logic with linked lists. In: Spin Workshop (2014)","DOI":"10.1145\/2632362.2632376"},{"key":"1_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-33125-1_10","volume-title":"Static Analysis","author":"A Thakur","year":"2012","unstructured":"Thakur, A., Elder, M., Reps, T.: Bilateral algorithms for symbolic abstraction. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 111\u2013128. Springer, Heidelberg (2012)"},{"key":"1_CR79","first-page":"15","volume":"311","author":"A Thakur","year":"2015","unstructured":"Thakur, A., Lal, A., Lim, J., Reps, T.: PostHat and all that: Automating abstract interpretation. ENTCS 311, 15\u201332 (2015)","journal-title":"ENTCS"},{"key":"1_CR80","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-642-14295-6_27","volume-title":"Computer Aided Verification","author":"A Thakur","year":"2010","unstructured":"Thakur, A., Lim, J., Lal, A., Burton, A., Driscoll, E., Elder, M., Andersen, T., Reps, T.: Directed proof generation for machine code. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 288\u2013305. Springer, Heidelberg (2010)"},{"key":"1_CR81","doi-asserted-by":"crossref","unstructured":"Thakur, A., Reps, T.: A generalization of St\u00e5lmarck\u2019s method. In: SAS (2012)","DOI":"10.1007\/978-3-642-33125-1_23"},{"key":"1_CR82","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. 7358, pp. 174\u2013192. Springer, Heidelberg (2012)"},{"issue":"11","key":"1_CR83","doi-asserted-by":"publisher","first-page":"1134","DOI":"10.1145\/1968.1972","volume":"27","author":"LG Valiant","year":"1984","unstructured":"Valiant, L.G.: A theory of the learnable. Commun. ACM 27(11), 1134\u20131142 (1984)","journal-title":"Commun. ACM"},{"issue":"3","key":"1_CR84","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1145\/373243.360206","volume":"36","author":"Eran Yahav","year":"2001","unstructured":"Yahav, E.: Verifying safety properties of concurrent Java programs using 3-valued logic. In: POPL (2001)","journal-title":"ACM SIGPLAN Notices"},{"key":"1_CR85","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. 2988, pp. 530\u2013545. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49122-5_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:25:33Z","timestamp":1559348733000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49122-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,25]]},"ISBN":["9783662491218","9783662491225"],"references-count":85,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49122-5_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,12,25]]},"assertion":[{"value":"25 December 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}