{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,25]],"date-time":"2026-03-25T12:05:34Z","timestamp":1774440334383,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":59,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540416357","type":"print"},{"value":"9783540445777","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44577-3_10","type":"book-chapter","created":{"date-parts":[[2007,6,9]],"date-time":"2007-06-09T18:23:39Z","timestamp":1181413419000},"page":"138-156","source":"Crossref","is-referenced-by-count":61,"title":["Abstract Interpretation Based Formal Methods and Future Challenges"],"prefix":"10.1007","author":[{"given":"Patrick","family":"Cousot","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,29]]},"reference":[{"issue":"1","key":"10_CR1","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/151646.151650","volume":"15","author":"R. Barbuti","year":"1993","unstructured":"R. Barbuti, R. Giacobazzi, and G. Levi. A general framework for semantics-based bottom-up abstract interpretation of logic programs. TOPLAS, 15(1):133\u2013181, 1993.","journal-title":"TOPLAS"},{"issue":"10","key":"10_CR2","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1145\/320385.320387","volume":"34","author":"B. Blanchet","year":"1999","unstructured":"B. Blanchet. Escape analysis for object-oriented languages: Application to Java. OOPSLA\u201999. SIGPLAN Not. 34(10):20\u201334, 1999.","journal-title":"OOPSLA\u201999. SIGPLAN Not."},{"issue":"2","key":"10_CR3","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1145\/316686.316688","volume":"21","author":"F. Bueno","year":"1999","unstructured":"F. Bueno, M.J. Garc\u00eda de la Banda, and M.V. Hermenegildo. Effectiveness of abstract interpretation in automatic parallelization: A case study in logic programming. TOPLAS, 21(2):189\u2013239, 1999.","journal-title":"TOPLAS"},{"key":"10_CR4","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0167-6423(86)90010-9","volume":"7","author":"G.L. Burn","year":"1986","unstructured":"G.L. Burn, C.L. Hankin, and S. Abramsky. Strictness analysis of higher-order functions. Sci. Comput. Programming, 7:249\u2013278, 1986.","journal-title":"Sci. Comput. Programming"},{"key":"10_CR5","unstructured":"M. Codish, D. Dams, G. Fil\u00e9, and M. Bruynooghe. Freeness analysis for logic programs-and correctness? Proc. ICLP\u2019 93, pp. 116\u2013131. MIT Press, 1993."},{"issue":"5","key":"10_CR6","doi-asserted-by":"publisher","first-page":"948","DOI":"10.1145\/330249.330252","volume":"21","author":"M. Codish","year":"1999","unstructured":"M. Codish, H. S\u00f8ndergaard, and P.J. Stuckey. Sharing and groundness dependencies in logic programs. TOPLAS, 21(5):948\u2013976, 1999.","journal-title":"TOPLAS"},{"issue":"3","key":"10_CR7","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/S0743-1066(98)10026-2","volume":"38","author":"A. Cortesi","year":"1999","unstructured":"A. Cortesi and G. Fil\u00e9. Sharing is optimal. J. Logic Programming, 38(3):371\u2013386, 1999.","journal-title":"J. Logic Programming"},{"issue":"1","key":"10_CR8","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/239912.239914","volume":"19","author":"A. Cortesi","year":"1997","unstructured":"A. Cortesi, G. Fil\u00e9, R. Giacobazzi, C. Palamidessi, and F. Ranzato. Complementation in abstract interpretation. TOPLAS, 19(1):7\u201347, 1997.","journal-title":"TOPLAS"},{"issue":"2","key":"10_CR9","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/0743-1066(95)00123-9","volume":"27","author":"A. Cortesi","year":"1996","unstructured":"A. Cortesi, G. Fil\u00e9, and W.H. Winsborough. Optimal groundness analysis using propositional logic. J. Logic Programming, 27(2):137\u2013167, 1996.","journal-title":"J. Logic Programming"},{"key":"10_CR10","unstructured":"P. Cousot. 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\u00e9se d\u2019\u00c9tat \u00e8s sciences math\u00e9matiques, Univ. of Grenoble, 1978."},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. ENTCS, 6, 1997. http:\/\/www.elsevier.nl\/locate\/entcs\/volume6.html , 25 pages.","DOI":"10.1016\/S1571-0661(05)80168-9"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"P. Cousot. Types as abstract interpretations. 24 th POPL, pp. 316\u2013331. ACM Press, 1997.","DOI":"10.1145\/263699.263744"},{"key":"10_CR13","unstructured":"P. Cousot. The calculational design of a generic abstract interpreter. In M. Broy and R. Steinbr\u00fcggen, editors, Calculational System Design, volume 173, pp. 421\u2013505. NATO Science Series, Series F: Computer and Systems Sciences. IOS Press, 1999."},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"P. Cousot. Partial completeness of abstract fixpoint checking. SARA\u20192000, LNAI 1864, pp. 1\u201325. Springer-Verlag, 2000.","DOI":"10.1007\/3-540-44914-0_1"},{"key":"10_CR15","unstructured":"P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoret. Comput. Sci., To appear (Preliminary version in [11])."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Static determination of dynamic properties of programs. 2 nd Int. Symp. on Programming, pp. 106\u2013130. Dunod, 1976.","DOI":"10.1145\/390019.808314"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. 4th POPL, pp. 238\u2013252. ACM Press, 1977.","DOI":"10.1145\/512950.512973"},{"issue":"8","key":"10_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/800228.806926","volume":"12","author":"P. Cousot","year":"1977","unstructured":"P. Cousot and R. Cousot. Automatic synthesis of optimal invariant assertions: mathematical foundations. Symp. on Artificial Intelligence & Programming Languages, SIGPLAN Not. 12(8):1\u201312, 1977.","journal-title":"Symp. on Artificial Intelligence & Programming Languages"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Systematic design of program analysis frameworks. 6th POPL, pp. 269\u2013282. ACM Press, 1979.","DOI":"10.1145\/567752.567778"},{"key":"10_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/3-540-10003-2_65","volume-title":"7th ICALP","author":"P. Cousot","year":"1980","unstructured":"P. Cousot and R. Cousot. Semantic analysis of communicating sequential processes. 7 th ICALP, LNCS 85, pp. 119\u2013133. Springer-Verlag, 1980."},{"key":"10_CR21","unstructured":"P. Cousot and R. Cousot. Invariance proof methods and analysis techniques for parallel programs. In A.W. Biermann, G. Guiho, and Y. Kodrato., editors, Automatic Program Construction Techniques, ch. 12, pp. 243\u2013271. Macmillan, 1984."},{"issue":"2-3","key":"10_CR22","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P. Cousot","year":"1992","unstructured":"P. Cousot and R. Cousot. Abstract interpretation and application to logic programs 4. J. Logic Programming, 13(2-3):103\u2013179, 1992.","journal-title":"J. Logic Programming"},{"issue":"4","key":"10_CR23","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"P. Cousot and R. Cousot. Abstract interpretation frameworks. J. Logic and Comp., 2(4):511\u2013547, Aug. 1992.","journal-title":"J. Logic and Comp."},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. 19 th POPL, pp. 83\u201394. ACM Press, 1992.","DOI":"10.1145\/143165.143184"},{"key":"10_CR25","unstructured":"P. Cousot and R. Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages). Proc. 1994 ICCL, pp. 95\u2013112. IEEE Comp. Soc. Press, 1994."},{"key":"10_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Proc. 4th PLILP\u201992","author":"P. Cousot","year":"1992","unstructured":"P. Cousot and R. Cousot. Comparing the Galois connection and widening\/ narrowing approaches to abstract interpretation. Proc. 4th PLILP\u201992, LNCS 631, pp. 269\u2013295. Springer-Verlag, 1992."},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. 7 th FPCA, pp. 170\u2013181. ACM Press, 1995.","DOI":"10.1145\/224164.224199"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Temporal abstract interpretation. 27 th POPL, pp. 12\u201325. ACM Press, 2000.","DOI":"10.1145\/325694.325699"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. 5 th POPL, pp. 84\u201397. ACM Press, 1978.","DOI":"10.1145\/512760.512770"},{"key":"10_CR30","unstructured":"DAEDALUS: Validation of critical software by static analysis and abstract testing. P. Cousot, R. Cousot, A. Deutsch, C. Ferdinand, \u00c9. Goubault, N. Jones, D. Pilaud, F. Randimbivololona, M. Sagiv, H. Seidel, and R. Wilhelm. Project IST-1999-20527 of the european 5th Framework Programme, Oct. 2000\u2013Oct. 2002."},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"S.K. Debray. Formal bases for data.ow analysis of logic programs. In G. Levi, editor, Advances in Logic Programming Theory, Int. Sec. 3, pp. 115\u2013182. Clarendon Press, 1994.","DOI":"10.1093\/oso\/9780198538530.003.0003"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"A. Deutsch. Semantic models and abstract interpretation techniques for inductive data structures and pointers. Proc. PEPM\u201995, pp. 226\u2013229. ACM Press, 1995.","DOI":"10.1145\/215465.215594"},{"key":"10_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/978-3-540-45099-3_7","volume-title":"Proc. SAS\u2019 2000","author":"N. Dor","year":"2000","unstructured":"N. Dor, M. Rodeh, and M. Sagiv. Checking cleanness in linked lists. Proc. SAS\u2019 2000, LNCS 1824, pp. 115\u2013134. Springer-Verlag, 2000."},{"issue":"1","key":"10_CR34","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/S0167-6423(99)00010-6","volume":"35","author":"C. Ferdinand","year":"1999","unstructured":"C. Ferdinand, F. Martin, R. Wilhelm, and M. Alt. Cache behavior prediction by abstract interpretation. Sci. Comput. Programming, 35(1):163\u2013189, 1999.","journal-title":"Sci. Comput. Programming"},{"key":"10_CR35","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-540-45099-3_8","volume-title":"Proc. SAS\u2019 2000","author":"J. Feret","year":"2000","unstructured":"J. Feret. Confidentiality analysis of mobile systems. Proc. SAS\u2019 2000, LNCS 1824, pp. 135\u2013154. Springer-Verlag, 2000."},{"issue":"2","key":"10_CR36","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"R. Giacobazzi","year":"2000","unstructured":"R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. J. ACM, 47(2):361\u2013416, 2000.","journal-title":"J. ACM"},{"key":"10_CR37","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1080\/00207168908803778","volume":"30","author":"P. Granger","year":"1989","unstructured":"P. Granger. Static analysis of arithmetical congruences. Int. J. Comput. Math., 30:165\u2013190, 1989.","journal-title":"Int. J. Comput. Math."},{"key":"10_CR38","first-page":"169","volume":"493","author":"P. Granger","year":"1991","unstructured":"P. Granger. Static analysis of linear congruence equalities among variables of a program. 493, pp. 169\u2013192. Springer-Verlag, 1991.","journal-title":"Static analysis of linear congruence equalities among variables of a program"},{"issue":"1","key":"10_CR39","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/S0167-6423(96)00041-X","volume":"31","author":"N. Halbwachs","year":"1998","unstructured":"N. Halbwachs. About synchronous programming and abstract interpretation. Sci. Comput. Programming, 31(1):75\u201389, 1998.","journal-title":"Sci. Comput. Programming"},{"key":"10_CR40","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-48294-6_9","volume-title":"Proc. SAS\u2019 99","author":"R.R. Hansen","year":"1999","unstructured":"R.R. Hansen, J.G. Jensen, F. Nielson, and H. Riis Nielson. Abstract interpretation of mobile ambients. Proc. SAS\u2019 99, LNCS 1694, pp. 134\u2013138. Springer-Verlag, 1999."},{"key":"10_CR41","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/BFb0032760","volume-title":"Proc. SAS\u2019 97","author":"W.L. Harrison","year":"1997","unstructured":"W.L. Harrison. Can abstract interpretation become a main stream compiler technology? (abstract). Proc. SAS\u2019 97, LNCS 1302, p. 395. Springer-Verlag, 1997."},{"key":"10_CR42","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1007\/978-3-540-45099-3_12","volume-title":"Proc. SAS\u2019 2000","author":"T.A. Henzinger","year":"2000","unstructured":"T.A. Henzinger, R. Majumbar, F. Mang, and J.-F. Raskin. Abstract interpretation of game properties. Proc. SAS\u2019 2000, LNCS 1824, pp. 220\u2013239. Springer-Verlag, 2000."},{"key":"10_CR43","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/BFb0032761","volume-title":"Proc. SAS\u2019 97","author":"N.D. Jones","year":"1997","unstructured":"N.D. Jones. Combining abstract interpretation and partial evaluation (brief overview). Proc. SAS\u2019 97, LNCS 1302, pp. 396\u2013405. Springer-Verlag, 1997."},{"key":"10_CR44","unstructured":"P. Lacan, J.N. Monfort, L.V.Q. Ribal, A. Deutsch, and G. Gonthier. The software reliability verification process: The Ariane 5 example. DASIA\u201998-DAta Systems In Aerospace, ESA Publications, 1998."},{"key":"10_CR45","doi-asserted-by":"crossref","unstructured":"B. Le Charlier and P. Van Hentenryck. Experimental evaluation of a generic abstract interpretation algorithm for Prolog. Proc. ICCL92, pp. 137\u2013146. IEEE Comp. Soc. Press, 1992.","DOI":"10.1109\/ICCL.1992.185476"},{"key":"10_CR46","volume-title":"Generating Program Analyzers","author":"F. Martin","year":"1999","unstructured":"F. Martin. Generating Program Analyzers. Pirrot Verlag, Saarbr\u00fccken, 1999."},{"key":"10_CR47","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/BFb0039705","volume-title":"FMPA","author":"F. Masdupuy","year":"1993","unstructured":"F. Masdupuy. Semantic analysis of interval congruences. FMPA, LNCS 735, pp. 142\u2013155. Springer-Verlag, 1993."},{"key":"10_CR48","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/978-3-540-45099-3_16","volume-title":"Proc. SAS\u2019 2000","author":"L. Mauborgne","year":"2000","unstructured":"L. Mauborgne. Tree schemata and fair termination. Proc. SAS\u2019 2000, LNCS 1824, pp. 302\u2013321. Springer-Verlag, 2000."},{"key":"10_CR49","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/978-3-540-45099-3_17","volume-title":"Proc. SAS\u2019 2000","author":"D. Monniaux","year":"2000","unstructured":"D. Monniaux. Abstract interpretation of probabilistic semantics. Proc. SAS\u2019 2000, LNCS 1824, pp. 322\u2013339. Springer-Verlag, 2000."},{"key":"10_CR50","unstructured":"A. Mycroft. Abstract Interpretation and Optimising Transformations for Applicative Programs. Ph.D. Dissertation, CST-15-81, Univ. of Edinburgh, 1981."},{"key":"10_CR51","unstructured":"F. Randimbivololona, J. Souyris, and A. Deutsch. Improving avionics software verification cost-effectiveness: Abstract interpretation based technology contribution. DASIA\u20192000-DAta Systems In Aerospace, ESA Publications, 2000."},{"key":"10_CR52","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/3-540-49727-7_22","volume-title":"Proc. SAS\u2019 98","author":"D.A. Schmidt","year":"1998","unstructured":"D.A. Schmidt and B. Steffen. Program analysis as model checking of abstract interpretations. Proc. SAS\u2019 98, LNCS 1503, pp. 351\u2013380. Springer-Verlag, 1998."},{"issue":"1","key":"10_CR53","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/0890-5401(92)90076-R","volume":"101","author":"J. Stransky","year":"1992","unstructured":"J. Stransky. A lattice for abstract interpretation of dynamic (lisp-like) structures. Inform. and Comput., 101(1):70\u2013102, 1992.","journal-title":"Inform. and Comput."},{"key":"10_CR54","unstructured":"TUAMOTU: Tatouage \u00e9lectronique s\u00e9mantique de code mobile Java. P. Cousot, R. Cousot, and M. Riguidel. Project RNRT 1999 n\u00b095, Oct. 1999\u2013Oct. 2001."},{"key":"10_CR55","unstructured":"R. Vall\u00e9e-Rai, H. Hendren, P. Lam, \u00c9 Gagnon, and P. Co. Soot-a Javatm optimization framework. Proc. CASCON\u2019 99, 1999."},{"key":"10_CR56","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-60360-3_52","volume-title":"Proc. SAS\u2019 95","author":"F. V\u00e9drine","year":"1995","unstructured":"F. V\u00e9drine. Binding-time analysis and strictness analysis by abstract interpretation. Proc. SAS\u2019 95, LNCS 983, pp. 400\u2013417. Springer-Verlag, 1995."},{"key":"10_CR57","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1007\/3-540-49727-7_9","volume-title":"Proc. SAS\u2019 98","author":"A. Venet","year":"1998","unstructured":"A. Venet. Automatic determination of communication topologies in mobile systems. Proc. SAS\u2019 98, LNCS 1503, pp. 152\u2013167. Springer-Verlag, 1998."},{"issue":"1","key":"10_CR58","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/S0167-6423(99)00012-X","volume":"35","author":"A. Venet","year":"1999","unstructured":"A. Venet. Automatic analysis of pointer aliasing for untyped programs. Sci. Comput. Programming, 35(1):223\u2013248, 1999.","journal-title":"Sci. Comput. Programming"},{"issue":"1","key":"10_CR59","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0167-6423(96)00044-5","volume":"31","author":"K. Yi","year":"1998","unstructured":"Kwangkeun Yi. An abstract interpretation for estimating uncaught exceptions in standard ML programs. Sci. Comput. Programming, 31(1):147\u2013173, 1998.","journal-title":"Sci. Comput. Programming"}],"container-title":["Lecture Notes in Computer Science","Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44577-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,15]],"date-time":"2024-02-15T00:37:00Z","timestamp":1707957420000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44577-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540416357","9783540445777"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/3-540-44577-3_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}