{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:14:15Z","timestamp":1763468055591},"reference-count":43,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2012,4,1]],"date-time":"2012-04-01T00:00:00Z","timestamp":1333238400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2016,4,27]],"date-time":"2016-04-27T00:00:00Z","timestamp":1461715200000},"content-version":"vor","delay-in-days":1487,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2012,4]]},"DOI":"10.1016\/j.tcs.2012.01.002","type":"journal-article","created":{"date-parts":[[2012,1,11]],"date-time":"2012-01-11T18:45:12Z","timestamp":1326307512000},"page":"23-42","source":"Crossref","is-referenced-by-count":4,"special_numbering":"C","title":["Inverse-limit and topological aspects of abstract interpretation"],"prefix":"10.1016","volume":"430","author":[{"given":"David A.","family":"Schmidt","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.tcs.2012.01.002_br000005","series-title":"Proc. 4th ACM Symp. on Principles of Programming Languages","first-page":"238","article-title":"Abstract interpretation: a unified lattice model for static analysis of programs","author":"Cousot","year":"1977"},{"key":"10.1016\/j.tcs.2012.01.002_br000010","series-title":"Proc. 6th ACM Symp. on Principles of Programming Languages","first-page":"269","article-title":"Systematic design of program analysis frameworks","author":"Cousot","year":"1979"},{"key":"10.1016\/j.tcs.2012.01.002_br000015","first-page":"527","article-title":"Abstract interpretation: a semantics-based tool for program analysis","volume":"vol. 4","author":"Jones","year":"1995"},{"key":"10.1016\/j.tcs.2012.01.002_br000020","series-title":"Program Flow Analysis","first-page":"303","article-title":"Semantic foundations of program analysis","author":"Cousot","year":"1981"},{"key":"10.1016\/j.tcs.2012.01.002_br000025","series-title":"Principles of Program Analysis","author":"Nielson","year":"1999"},{"key":"10.1016\/j.tcs.2012.01.002_br000030","series-title":"Proc. 5th ACM Symp. on Principles of Programming Languages","first-page":"84","article-title":"Automatic discovery of linear restraints among variables of a program","author":"Cousot","year":"1978"},{"key":"10.1016\/j.tcs.2012.01.002_br000035","series-title":"Proc. Conf. Computer Aided Verification","first-page":"72","article-title":"Construction of abstract state graphs with pvs","volume":"vol. 1254","author":"Graf","year":"1997"},{"key":"10.1016\/j.tcs.2012.01.002_br000040","series-title":"Proc. ICALP\u201983","first-page":"662","article-title":"Powerdomains and predicate transformers: a topological view","volume":"vol. 154","author":"Smyth","year":"1983"},{"key":"10.1016\/j.tcs.2012.01.002_br000045","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1145\/333979.333989","article-title":"Making abstract interpretations complete","volume":"47","author":"Giacobazzi","year":"2000","journal-title":"Journal of the ACM"},{"key":"10.1016\/j.tcs.2012.01.002_br000050","series-title":"Static Analysis Symposium","first-page":"356","article-title":"Incompleteness, counterexamples, and refinements in abstract model checking","volume":"vol. 2126","author":"Giacobazzi","year":"2001"},{"key":"10.1016\/j.tcs.2012.01.002_br000055","series-title":"Asian Symp. Prog. Lang. Systems","first-page":"183","article-title":"Comparing completeness properties of static analyses and their logics","volume":"vol. 4279","author":"Schmidt","year":"2006"},{"key":"10.1016\/j.tcs.2012.01.002_br000060","series-title":"Semantics of Programming Languages","author":"Gunter","year":"1992"},{"key":"10.1016\/j.tcs.2012.01.002_br000065","unstructured":"G. Plotkin, Domains, Lecture notes, Univ. Pisa\/Edinburgh, 1983."},{"key":"10.1016\/j.tcs.2012.01.002_br000070","unstructured":"P. Cousot, R. Cousot, Higher-order abstract interpretation, in: Proceedings IEEE Int. Conf. Computer Lang., 1994."},{"key":"10.1016\/j.tcs.2012.01.002_br000075","series-title":"Proc. European Symp. Programming","first-page":"18","article-title":"Strong preservation as completeness in abstract interpretation","volume":"vol. 2986","author":"Ranzato","year":"2004"},{"key":"10.1016\/j.tcs.2012.01.002_br000080","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","article-title":"The octagon abstract domain","volume":"19","author":"Min\u00e9","year":"2006","journal-title":"Journal of Higher-Order and Symbolic Computation"},{"key":"10.1016\/j.tcs.2012.01.002_br000085","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/s10009-002-0095-0","article-title":"Boolean and cartesian abstraction for model checking C programs","volume":"5","author":"Ball","year":"2003","journal-title":"Journal of Software Tools for Technology Transfer"},{"key":"10.1016\/j.tcs.2012.01.002_br000090","doi-asserted-by":"crossref","unstructured":"N. Jones, S. Muchnick, Flow analysis and optimization of LISP-like structures, in: Proc. 6th. ACM Symp. Principles of Programming Languages, 1979, pp. 244\u2013256.","DOI":"10.1145\/567752.567776"},{"key":"10.1016\/j.tcs.2012.01.002_br000095","series-title":"Continuous Lattices and Domains","author":"Gierz","year":"2003"},{"key":"10.1016\/j.tcs.2012.01.002_br000100","unstructured":"J. Reynolds, Notes on a lattice-theoretic approach to the theory of computation, Technical report, Computer Science, Syracuse University, 1972."},{"key":"10.1016\/j.tcs.2012.01.002_br000105","series-title":"Stone Spaces","author":"Johnstone","year":"1986"},{"key":"10.1016\/j.tcs.2012.01.002_br000110","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0168-0072(91)90065-T","article-title":"Domain theory in logical form","volume":"51","author":"Abramsky","year":"1991","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/j.tcs.2012.01.002_br000115","series-title":"Program Flow Analysis: Theory and Applications","article-title":"Denotational definition of properties of program\u2019s computations","author":"Donzeau-Gouge","year":"1981"},{"key":"10.1016\/j.tcs.2012.01.002_br000120","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BF00263194","article-title":"A denotational framework for data flow analysis","volume":"18","author":"Nielson","year":"1982","journal-title":"Acta Informatica"},{"key":"10.1016\/j.tcs.2012.01.002_br000125","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1145\/3916.3917","article-title":"Program transformations in a denotational setting","volume":"7","author":"Nielson","year":"1985","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/j.tcs.2012.01.002_br000130","series-title":"Two-Level Functional Languages","author":"Nielson","year":"1992"},{"key":"10.1016\/j.tcs.2012.01.002_br000135","doi-asserted-by":"crossref","unstructured":"N. Jones, A. Mycroft, Data flow analysis of applicative programs using minimal function graphs, in: Proc. 13th ACM Symp. on Principles of Prog. Languages, 1986, pp. 296\u2013306.","DOI":"10.1145\/512644.512672"},{"key":"10.1016\/j.tcs.2012.01.002_br000140","series-title":"Formal Description of Programming Concepts","first-page":"238","article-title":"Static determination of dynamic properties of recursive procedures","author":"Cousot","year":"1978"},{"key":"10.1016\/j.tcs.2012.01.002_br000145","doi-asserted-by":"crossref","unstructured":"S. Hunt, Frontiers and open sets in abstract intepretation, in: Proc. ACM Symp. Functional Prog. and Comp. Architecture, 1989, pp. 194\u2013216.","DOI":"10.1145\/99370.99371"},{"key":"10.1016\/j.tcs.2012.01.002_br000150","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0890-5401(91)90004-L","article-title":"Inverse image analysis generalises strictness analysis","volume":"90","author":"Dybjer","year":"1991","journal-title":"Information and Computation"},{"key":"10.1016\/j.tcs.2012.01.002_br000155","unstructured":"T. Jensen, Abstract interpretation in logical form, Ph.D. Thesis, Imperial College, London, 1992."},{"key":"10.1016\/j.tcs.2012.01.002_br000160","doi-asserted-by":"crossref","unstructured":"N. Benton, Strictness logic and polymorphic invariance, in: Proc. Logical Found. Comp. Sci, 1992, pp. 33\u201344.","DOI":"10.1007\/BFb0023861"},{"key":"10.1016\/j.tcs.2012.01.002_br000165","series-title":"General Topology","author":"Willard","year":"2004"},{"key":"10.1016\/j.tcs.2012.01.002_br000170","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","article-title":"Parametric shape analysis via 3-valued logic","volume":"24","author":"Sagiv","year":"2002","journal-title":"ACM TOPLAS"},{"key":"10.1016\/j.tcs.2012.01.002_br000175","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01384313","article-title":"Property preserving abstractions for verification of concurrent systems","volume":"6","author":"Loiseaux","year":"1995","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/j.tcs.2012.01.002_br000180","series-title":"Handbook of Theoretical Computer Science: Vol. B","first-page":"633","article-title":"Semantic domains","author":"Gunter","year":"1990"},{"key":"10.1016\/j.tcs.2012.01.002_br000185","unstructured":"R. Heckmann, Power domain constructions, Ph.D. Thesis, Univ. Saarbr\u00fccken, 1990."},{"key":"10.1016\/j.tcs.2012.01.002_br000190","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/0022-0000(78)90048-X","article-title":"Powerdomains","volume":"16","author":"Smyth","year":"1978","journal-title":"Journal of Computer and System Sciences"},{"key":"10.1016\/j.tcs.2012.01.002_br000195","series-title":"Proc. SAS\u201995","article-title":"Optimality in abstractions of model checking","volume":"vol. 983","author":"Cleaveland","year":"1995"},{"key":"10.1016\/j.tcs.2012.01.002_br000200","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/244795.244800","article-title":"Abstract interpretation of reactive systems","volume":"19","author":"Dams","year":"1997","journal-title":"ACM Transactions on Programming Language Systems"},{"key":"10.1016\/j.tcs.2012.01.002_br000205","series-title":"Proc. Symp. Static Analysis","first-page":"127","article-title":"Underapproximating predicate transformers","volume":"vol. 4134","author":"Schmidt","year":"2006"},{"key":"10.1016\/j.tcs.2012.01.002_br000210","series-title":"Proc. Logic in Computer Science","first-page":"108","article-title":"Equation solving using modal transition systems","author":"Larsen","year":"1990"},{"key":"10.1016\/j.tcs.2012.01.002_br000215","doi-asserted-by":"crossref","first-page":"1313","DOI":"10.1016\/j.ic.2008.07.004","article-title":"Three-valued abstraction: more precision at less cost","volume":"206","author":"Shoham","year":"1998","journal-title":"Information and Computation"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397512000175?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397512000175?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,6,22]],"date-time":"2019-06-22T06:38:26Z","timestamp":1561185506000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397512000175"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4]]},"references-count":43,"alternative-id":["S0304397512000175"],"URL":"https:\/\/doi.org\/10.1016\/j.tcs.2012.01.002","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2012,4]]}}}