{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T16:49:34Z","timestamp":1725814174977},"publisher-location":"Berlin, Heidelberg","reference-count":68,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662460801"},{"type":"electronic","value":"9783662460818"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46081-8_2","type":"book-chapter","created":{"date-parts":[[2014,12,11]],"date-time":"2014-12-11T04:25:44Z","timestamp":1418271944000},"page":"19-42","source":"Crossref","is-referenced-by-count":19,"title":["Abstracting Induction by Extrapolation and Interpolation"],"prefix":"10.1007","author":[{"given":"Patrick","family":"Cousot","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1007\/978-3-642-31424-7_48","volume-title":"Computer Aided Verification","author":"A. Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: UFO: A framework for abstraction- and interpolation-based software verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 672\u2013678. Springer, Heidelberg (2012)"},{"issue":"1-2","key":"2_CR2","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1016\/j.scico.2005.02.003","volume":"58","author":"R. Bagnara","year":"2005","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Sci. Comput. Program.\u00a058(1-2), 28\u201356 (2005)","journal-title":"Sci. Comput. Program."},{"issue":"3-4","key":"2_CR3","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/s10009-007-0029-y","volume":"9","author":"R. Bagnara","year":"2007","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. STTT\u00a09(3-4), 413\u2013414 (2007)","journal-title":"STTT"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS\/ETAPS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-540-71067-7_15","volume-title":"Theorem Proving in Higher Order Logics","author":"S. B\u00f6hme","year":"2008","unstructured":"B\u00f6hme, S., Leino, K.R.M., Wolff, B.: HOL-Boogie \u2014 An interactive prover for the Boogie program-verifier. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 150\u2013166. Springer, Heidelberg (2008)"},{"key":"2_CR6","unstructured":"Burstall, R.M.: Program proving as hand simulation with a little induction. In: IFIP Congress, pp. 308\u2013312 (1974)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Sankaranarayanan, S.: Expectation invariants for probabilistic program loops as fixed points. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol.\u00a08723, pp. 85\u2013100. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-319-10936-7_6"},{"issue":"1","key":"2_CR8","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/1838552.1838559","volume":"12","author":"A. Cimatti","year":"2010","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log.\u00a012(1), 7 (2010)","journal-title":"ACM Trans. Comput. Log."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Colby, C., Lee, P.: Trace-based program analysis. In: POPL, pp. 195\u2013207. ACM (1996)","DOI":"10.1145\/237721.237776"},{"issue":"1","key":"2_CR10","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/239912.239914","volume":"19","author":"A. Cortesi","year":"1997","unstructured":"Cortesi, A., Fil\u00e9, G., Giacobazzi, R., Palamidessi, C., Ranzato, F.: Complementation in abstract interpretation. ACM TOPLAS\u00a019(1), 7\u201347 (1997)","journal-title":"ACM TOPLAS"},{"key":"2_CR11","unstructured":"Cousot, P.: M\u00e9thodes it\u00e9ratives de construction et d\u2019approximation de points fixes d\u2019op\u00e9rateurs monotones sur un treillis, analyse s\u00e9mantique de programmes. Th\u00e8se d\u2019\u00c9tat \u00e8s sciences math\u00e9matiques, Universit\u00e9 Joseph Fourier, Grenoble, France (March 21, 1978)"},{"key":"2_CR12","unstructured":"Cousot, P., Cousot, R.: Static verification of dynamic type properties of variables. Research Report R.R. 25, Laboratoire IMAG, Universit\u00e9 Joseph Fourier, Grenoble, France (November 1975)"},{"key":"2_CR13","first-page":"106","volume-title":"Proc. Secont Int. Symp. on Programming","author":"P. Cousot","year":"1976","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proc. Secont Int. Symp. on Programming, pp. 106\u2013130. Dunod, Paris (1976)"},{"issue":"1","key":"2_CR14","doi-asserted-by":"publisher","first-page":"43","DOI":"10.2140\/pjm.1979.82.43","volume":"82","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Constructive versions of Tarski\u2019s fixed point theorems. Pacific J. of Math.\u00a082(1), 43\u201357 (1979)","journal-title":"Pacific J. of Math."},{"key":"2_CR15","unstructured":"Cousot, P., Cousot, R.: Induction principles for proving invariance properties of programs. In: Tools & Notions for Program Construction: An Advanced Course, pp. 75\u2013119. Cambridge University Press (August 1982)"},{"key":"2_CR16","unstructured":"Cousot, P.: Semantic foundations of program analysis. In: Program Flow Analysis: Theory and Applications, ch. 10, pp. 303\u2013342. Prentice-Hall (1981)"},{"key":"2_CR17","first-page":"841","volume-title":"Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B)","author":"P. Cousot","year":"1990","unstructured":"Cousot, P.: Methods and logics for proving programs. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 841\u2013994. Elsevier, North-Holland (1990)"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-540-39910-0_11","volume-title":"Verification: Theory and Practice","author":"P. Cousot","year":"2004","unstructured":"Cousot, P.: Verification by abstract interpretation. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 243\u2013268. Springer, Heidelberg (2004)"},{"key":"2_CR19","unstructured":"Cousot, P., Cousot, R.: V\u00e9rification statique de la coh\u00e9rence dynamique des programmes. Rapport du contrat IRIA SESORI No 75-035, Laboratoire IMAG, Universit\u00e9 Joseph Fourier, Grenoble, France, 125 p. (Septembr 23, 1975)"},{"key":"2_CR20","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, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282. ACM (1979)","DOI":"10.1145\/567752.567778"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Programming Language Implementation and Logic Programming","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol.\u00a0631, pp. 269\u2013295. Springer, Heidelberg (1992)"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/BFb0039703","volume-title":"Formal Methods in Programming and Their Applications","author":"P. Cousot","year":"1993","unstructured":"Cousot, P., Cousot, R.: Galois connection based abstract interpretations for strictness analysis. In: Bjorner, D., Broy, M., Pottosin, I.V. (eds.) FMP&TA 1993. LNCS, vol.\u00a0735, pp. 98\u2013127. Springer, Heidelberg (1993)"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In: FPCA, pp. 170\u2013181. ACM (1995)","DOI":"10.1145\/224164.224199"},{"issue":"44","key":"2_CR25","doi-asserted-by":"publisher","first-page":"6135","DOI":"10.1016\/j.tcs.2011.06.005","volume":"412","author":"P. Cousot","year":"2011","unstructured":"Cousot, P., Cousot, R.: Grammar semantics, analysis and parsing by abstract interpretation. TCS\u00a0412(44), 6135\u20136192 (2011)","journal-title":"TCS"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: An abstract interpretation framework for termination. In: POPL, pp. 245\u2013258. ACM (2012)","DOI":"10.1145\/2103621.2103687"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: A Galois connection calculus for abstract interpretation. In: POPL, pp. 3\u20134. ACM (2014)","DOI":"10.1145\/2535838.2537850"},{"issue":"3","key":"2_CR28","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10703-009-0089-6","volume":"35","author":"P. Cousot","year":"2009","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Why does Astr\u00e9e scale up? Formal Methods in System Design\u00a035(3), 229\u2013264 (2009)","journal-title":"Formal Methods in System Design"},{"issue":"6","key":"2_CR29","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/2395116.2395120","volume":"59","author":"P. Cousot","year":"2012","unstructured":"Cousot, P., Cousot, R., Mauborgne, L.: Theories, solvers and static analysis by abstract interpretation. J. ACM\u00a059(6), 31 (2012)","journal-title":"J. ACM"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84\u201396. ACM (1978)","DOI":"10.1145\/512760.512770"},{"issue":"3","key":"2_CR31","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. Journal of Symbolic Logic\u00a022(3), 269\u2013285 (1957)","journal-title":"Journal of Symbolic Logic"},{"issue":"3","key":"2_CR32","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0020-0190(94)00196-6","volume":"53","author":"E.W. Dijkstra","year":"1995","unstructured":"Dijkstra, E.W.: Heuristics for a calculational proof. Inf. Process. Lett.\u00a053(3), 141\u2013143 (1995)","journal-title":"Inf. Process. Lett."},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. Texts and monographs in computer science. Springer (1990)","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.L.: Inductive invariant generation via abductive inference. In: OOPSLA, pp. 443\u2013456. ACM (2013)","DOI":"10.1145\/2544173.2509511"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Abstract satisfaction. In: POPL, pp. 139\u2013150. ACM (2014)","DOI":"10.1145\/2535838.2535868"},{"issue":"6","key":"2_CR36","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1145\/1857914.1857917","volume":"57","author":"J. Esparza","year":"2010","unstructured":"Esparza, J., Kiefer, S., Luttenberger, M.: Newtonian program analysis. J. ACM\u00a057(6), 33 (2010)","journal-title":"J. ACM"},{"issue":"3","key":"2_CR37","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s11229-008-9354-2","volume":"164","author":"S. Feferman","year":"2008","unstructured":"Feferman, S.: Harmonious logic: Craig\u2019s interpolation theorem and its descendants. Synthese\u00a0164(3), 341\u2013357 (2008)","journal-title":"Synthese"},{"key":"2_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-24725-8_4","volume-title":"Programming Languages and Systems","author":"J. Feret","year":"2004","unstructured":"Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 33\u201348. Springer, Heidelberg (2004)"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI, pp. 234\u2013245. ACM (2002)","DOI":"10.1145\/543552.512558"},{"issue":"4S","key":"2_CR40","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/2502508.2502520","volume":"48","author":"C. Flanagan","year":"2013","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: PLDI 2002: Extended static checking for Java. SIGPLAN Notices\u00a048(4S), 22\u201333 (2013)","journal-title":"SIGPLAN Notices"},{"key":"2_CR41","doi-asserted-by":"crossref","unstructured":"Floyd, R.: Assigning meaning to programs. In: Proc. Symposium in Applied Mathematics, vol.\u00a019, pp. 19\u201332. Amer. Math. Soc. (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Gange, G., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: Abstract interpretation over non-lattice abstract domains. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol.\u00a07935, pp. 6\u201324. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-38856-9_3"},{"key":"2_CR43","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":"2_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-540-78800-3_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B.S. Gulavani","year":"2008","unstructured":"Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically refining abstract interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 443\u2013458. Springer, Heidelberg (2008)"},{"key":"2_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-642-33125-1_15","volume-title":"Static Analysis","author":"N. Halbwachs","year":"2012","unstructured":"Halbwachs, N., Henry, J.: When the decreasing sequence fails. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 198\u2013213. Springer, Heidelberg (2012)"},{"issue":"2","key":"2_CR46","first-page":"157","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y., Roumanoff, P.: Verification of real-time systems using linear relation analysis. FMSD\u00a011(2), 157\u2013185 (1997)","journal-title":"FMSD"},{"issue":"10","key":"2_CR47","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. C. ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"C. ACM"},{"key":"2_CR48","doi-asserted-by":"crossref","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Playing in the grey area of proofs. In: POPL, pp. 259\u2013272. ACM (2012)","DOI":"10.1145\/2103621.2103689"},{"key":"2_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/BFb0030832","volume-title":"Computing and Combinatorics","author":"G. Huang","year":"1995","unstructured":"Huang, G.: Constructing Craig interpolation formulas. In: Li, M., Du, D.-Z. (eds.) COCOON 1995. LNCS, vol.\u00a0959, pp. 181\u2013190. Springer, Heidelberg (1995)"},{"key":"2_CR50","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: POPL, pp. 529\u2013540. ACM (2014)","DOI":"10.1145\/2535838.2535843"},{"issue":"4","key":"2_CR51","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/359461.359466","volume":"20","author":"J.H. Morris Jr.","year":"1977","unstructured":"Morris Jr., J.H., Wegbreit, B.: Subgoal induction. C. ACM\u00a020(4), 209\u2013222 (1977)","journal-title":"C. ACM"},{"key":"2_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-642-24372-1_38","volume-title":"Automated Technology for Verification and Analysis","author":"L. Lakhdar-Chaouch","year":"2011","unstructured":"Lakhdar-Chaouch, L., Jeannet, B., Girault, A.: Widening with thresholds for programs with complex control graphs. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 492\u2013502. Springer, Heidelberg (2011)"},{"key":"2_CR53","doi-asserted-by":"publisher","first-page":"3","DOI":"10.4204\/EPTCS.149.2","volume":"149","author":"K.R.M. Leino","year":"2014","unstructured":"Leino, K.R.M., W\u00fcstholz, V.: The Dafny integrated development environment. F-IDE. EPTCS\u00a0149, 3\u201315 (2014)","journal-title":"F-IDE. EPTCS"},{"key":"2_CR54","doi-asserted-by":"crossref","unstructured":"Logozzo, F., Lahiri, S.K., F\u00e4hndrich, M., Blackshear, S.: Verification modulo versions: Towards usable verification. In: PLDI, p. 32. ACM (2014)","DOI":"10.1145\/2594291.2594326"},{"key":"2_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"2_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-31980-1_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: Applications of Craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 1\u201312. Springer, Heidelberg (2005)"},{"issue":"1","key":"2_CR57","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. TCS\u00a0345(1), 101\u2013121 (2005)","journal-title":"TCS"},{"key":"2_CR58","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Widening and interpolation. In: Yahav, E. (ed.) SAS 2011. LNCS, vol.\u00a06887, p. 1. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-23702-7_1"},{"key":"2_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/3-540-61739-6_53","volume-title":"Static Analysis","author":"A. Venet","year":"1996","unstructured":"Venet, A.: Abstract cofibered domains: Application to the alias analysis of untyped programs. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol.\u00a01145, pp. 366\u2013382. Springer, Heidelberg (1996)"},{"key":"2_CR60","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.jalgebra.2013.11.019","volume":"402","author":"G. Metcalfe","year":"2014","unstructured":"Metcalfe, G., Montagna, F., Tsinakis, C.: Amalgamation and interpolation in ordered algebras. J. of Algebra\u00a0402, 21\u201382 (2014)","journal-title":"J. of Algebra"},{"key":"2_CR61","doi-asserted-by":"crossref","unstructured":"Mycroft, A.: The theory and practice of transforming call-by-need into call-by-value. In: Salinesi, C., Pastor, O. (eds.) CAiSE Workshops 2011. LNCS, vol.\u00a083, pp. 269\u2013281. Springer, Heidelberg (2011)","DOI":"10.1007\/3-540-09981-6_19"},{"key":"2_CR62","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/BF01966091","volume":"6","author":"P. Naur","year":"1966","unstructured":"Naur, P.: Proofs of algorithms by general snapshots. BIT\u00a06, 310\u2013316 (1966)","journal-title":"BIT"},{"key":"2_CR63","doi-asserted-by":"crossref","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. TOPLAS 29(5) (2007)","DOI":"10.1145\/1275497.1275501"},{"key":"2_CR64","doi-asserted-by":"crossref","unstructured":"Scott, D.S.: Continuous lattices. In: Toposes, Algebraic Geometry and Logic. LNM, vol.\u00a0274, Springer (1972)","DOI":"10.1007\/BFb0073967"},{"key":"2_CR65","unstructured":"Scott, D., Strachey, C.: Towards a mathematical semantics for computer languages. Technical Report PRG-6, Oxford University Computer Laboratory (August 1971)"},{"key":"2_CR66","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Tarski, A.: A lattice theoretical fixpoint theorem and its applications. Pacific J. of Math.\u00a05, 285\u2013310 (1955)","journal-title":"Pacific J. of Math."},{"key":"2_CR67","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.\u00a07460, pp. 111\u2013128. Springer, Heidelberg (2012)"},{"key":"2_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/3-540-61739-6_53","volume-title":"Static Analysis","author":"A. Venet","year":"1996","unstructured":"Venet, A.: Abstract cofibered domains: Application to the alias analysis of untyped programs. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol.\u00a01145, pp. 366\u2013382. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46081-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T20:27:21Z","timestamp":1559075241000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46081-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662460801","9783662460818"],"references-count":68,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46081-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}