{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:11:44Z","timestamp":1763467904628},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540938996"},{"type":"electronic","value":"9783540939009"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-93900-9_22","type":"book-chapter","created":{"date-parts":[[2008,12,15]],"date-time":"2008-12-15T04:35:59Z","timestamp":1229315759000},"page":"260-274","source":"Crossref","is-referenced-by-count":15,"title":["A Posteriori Soundness for Non-deterministic Abstract Interpretations"],"prefix":"10.1007","author":[{"given":"Matthew","family":"Might","sequence":"first","affiliation":[]},{"given":"Panagiotis","family":"Manolios","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-49538-X_2","volume-title":"ECOOP \u201995 - Object-Oriented Programming","author":"O. Agesen","year":"1995","unstructured":"Agesen, O.: The cartesian product algorithm: Simple and precise type inference of parametric polymorphism. In: Olthoff, W. (ed.) ECOOP 1995. LNCS, vol.\u00a0952, pp. 2\u201326. Springer, Heidelberg (1995)"},{"key":"22_CR2","unstructured":"Andersen, L.O.: Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen (May 1994)"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/11823230_15","volume-title":"Static Analysis","author":"G. Balakrishnan","year":"2006","unstructured":"Balakrishnan, G., Reps, T.: Recency-abstraction for heap-allocated storage. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 221\u2013239. Springer, Heidelberg (2006)"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Chase, D.R., Wegman, M., Zadeck, F.K.: Analysis of Pointers and Structures. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, White Plains, New York, June 1990, pp. 296\u2013310 (1990)","DOI":"10.1145\/93542.93585"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Electronic Notes in Theoretical Computer Science\u00a06, 25 pages (1997), http:\/\/www.elsevier.nl\/locate\/entcs\/volume6.html","DOI":"10.1016\/S1571-0661(05)80168-9"},{"key":"22_CR6","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, California, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"22_CR7","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1145\/567752.567778","volume-title":"Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, Texas, pp. 269\u2013282. ACM Press, New York (1979)"},{"issue":"4","key":"22_CR8","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation\u00a02(4), 511\u2013547 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/3-540-45587-6_16","volume-title":"Practical Aspects of Declarative Languages","author":"J. Gallagher","year":"2002","unstructured":"Gallagher, J., Gallagher, J.P., Puebla, G., Puebla, G.: Abstract interpretation over non-deterministic finite tree automata for set-based analysis of logic programs. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds.) PADL 2002. LNCS, vol.\u00a02257, pp. 243\u2013261. Springer, Heidelberg (2002)"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Program analysis using random interpretation. Ph.D. Dissertation, UC-Berkeley (2005)","DOI":"10.1145\/1047659.1040332"},{"issue":"3\/4","key":"22_CR11","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/BF01808954","volume":"2","author":"W.L. Harrison","year":"1989","unstructured":"Harrison, W.L.: The interprocedural analysis and automatic parallelization of Scheme programs. Lisp and Symbolic Computation\u00a02(3\/4), 179\u2013396 (1989)","journal-title":"Lisp and Symbolic Computation"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Hudak, P.: A semantic model of reference counting and its abstraction (detailed summary). In: Proceedings of the 1986 ACM Conference on LISP and Functional Programming, Cambridge, Massachusetts, August 1986, pp. 351\u2013363 (1986)","DOI":"10.1145\/319838.319876"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-540-24611-4_12","volume-title":"Validation of Stochastic Systems","author":"M. Huth","year":"2004","unstructured":"Huth, M.: An abstraction framework for mixed non-deterministic and probabilistic systems. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol.\u00a02925, pp. 419\u2013444. Springer, Heidelberg (2004)"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Jagannathan, S., Thiemann, P., Weeks, S., Wright, A.K.: Single and loving it: Must-alias analysis for higher-order languages. In: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California, January 1998, pp. 329\u2013341 (1998)","DOI":"10.1145\/268946.268973"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-10843-2_10","volume-title":"Automata, Languages and Programming","author":"N.D. Jones","year":"1981","unstructured":"Jones, N.D.: Flow analysis of lambda expressions (preliminary version). In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol.\u00a0115, pp. 114\u2013128. Springer, Heidelberg (1981)"},{"key":"22_CR16","first-page":"66","volume-title":"Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"N.D. Jones","year":"1982","unstructured":"Jones, N.D., Muchnick, S.S.: A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 66\u201374. ACM, New York (1982)"},{"key":"22_CR17","unstructured":"Might, M.: Environment Analysis of Higher-Order Languages. PhD thesis, Georgia Institute of Technology (2007)"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Might, M., Shivers, O.: Environment analysis via \u0394CFA. In: Proceedings of the 33rd Annual ACM Symposium on the Principles of Programming Languages (POPL 2006), Charleston, South Carolina, January 2006, pp. 127\u2013140 (2006)","DOI":"10.1145\/1111320.1111049"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Might, M., Shivers, O.: Improving flow analyses via \u0393CFA: Abstract garbage collection and counting. In: Proceedings of the 11th ACM International Conference on Functional Programming (ICFP 2006), Portland, Oregon, September 2006, pp. 13\u201325 (2006)","DOI":"10.1145\/1160074.1159807"},{"issue":"1\u20133","key":"22_CR20","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/j.tcs.2006.12.031","volume":"375","author":"M. Might","year":"2007","unstructured":"Might, M., Shivers, O.: Analyzing the environment structure of higher-order languages using frame strings. Theoretical Computer Science\u00a0375(1\u20133), 137\u2013168 (2007)","journal-title":"Theoretical Computer Science"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Might, M., Shivers, O.: Exploiting reachability and cardinality in abstract interpretation. Journal of Functional Programming (2008)","DOI":"10.1017\/S0956796808006941"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Symposium on Principles of Programming Languages, pp. 105\u2013118 (1999)","DOI":"10.1145\/292540.292552"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Shivers, O.: Control-flow analysis in Scheme. In: Proceedings of the SIGPLAN 1988 Conference on Programming Language Design and Implementation (PLDI), Atlanta, Georgia, June 1988, pp. 164\u2013174 (1988)","DOI":"10.1145\/53990.54007"},{"key":"22_CR24","unstructured":"Shivers, O.: Control-Flow Analysis of Higher-Order Languages. PhD thesis, School of Computer Science, Carnegie-Mellon University, Pittsburgh, Pennsylvania, Technical Report CMU-CS-91-145 (May 1991)"},{"issue":"1","key":"22_CR25","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1145\/271510.271523","volume":"20","author":"A.K. Wright","year":"1998","unstructured":"Wright, A.K., Jagannathan, S.: Polymorphic splitting: An effective polyvariant flow analysis. ACM Transactions on Programming Languages and Systems\u00a020(1), 166\u2013207 (1998)","journal-title":"ACM Transactions on Programming Languages and Systems"}],"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-540-93900-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T04:11:32Z","timestamp":1557979892000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-93900-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540938996","9783540939009"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-93900-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}