{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214122},"publisher-location":"Berlin, Heidelberg","reference-count":53,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540650140"},{"type":"electronic","value":"9783540497271"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49727-7_22","type":"book-chapter","created":{"date-parts":[[2007,6,6]],"date-time":"2007-06-06T23:02:49Z","timestamp":1181170969000},"page":"351-380","source":"Crossref","is-referenced-by-count":61,"title":["Program Analysis as Model Checking of Abstract Interpretations"],"prefix":"10.1007","author":[{"given":"David","family":"Schmidt","sequence":"first","affiliation":[]},{"given":"Bernhard","family":"Steffen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,24]]},"reference":[{"key":"22_CR1","series-title":"Lecture Notes","volume-title":"Non-Well-Founded Sets","author":"P. Aczel","year":"1988","unstructured":"P. Aczel. Non-Well-Founded Sets, Lecture Notes 14, Center for Study of Language and Information, Stanford, CA, 1988."},{"key":"22_CR2","series-title":"Lect Notes Comput Sci","first-page":"260","volume-title":"Property preserving simulations","author":"S. Bensalem","year":"1992","unstructured":"S. Bensalem and A. Bouajjani and C. Loiseaux and J. Sifakis. Property preserving simulations. Computer Aided Verification: CAV\u201992. Lecture Notes in Computer Science 663, Springer, 1992, 260\u2013273."},{"key":"22_CR3","unstructured":"D. Berry. Generating Program Animators from Programming Language Semantics, Ph.D. Thesis, LFCS Report ECS-LFCS-91-148, University of Edinburgh, 1991."},{"key":"22_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Model Checking for Context-Free Processes","author":"O. Burkart","year":"1992","unstructured":"O. Burkart and B. Steffen. Model Checking for Context-Free Processes. Proceedings of the International Conference on Concurrency Theory, Concur95, LNCS 630, 1992"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"S. C. Cheung and J. Kramer. An Integrated Method For Effective Behaviour Analysis of Distributed Systems. Proceedings of the 16th International Conference on Software Engineering, Sorrento, CA, USA, 1994, pp. 309\u2013320.","DOI":"10.1109\/ICSE.1994.296793"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"S. C. Cheung and J. Kramer. Tractable Flow Analysis for Distributed Systems. IEEE Transactions on Software Engineering 20-9 (1994).","DOI":"10.1109\/32.310668"},{"key":"22_CR7","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"E. Clarke and E. Emerson and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8 (1986) 244\u2013263.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"22_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/BFb0028174","volume-title":"A Decade of Concurrency: Reflections and Perspectives","author":"E.M. Clarke","year":"1993","unstructured":"E.M. Clarke and O. Grumberg and D.E. Long. Verification tools for finite-state concurrent systems. In A Decade of Concurrency: Reflections and Perspectives, J.W. deBakker and W.-P. deRoever and G. Rozenberg\u201d, editors, Springer LNCS 803, 1993, pp. 124\u2013175."},{"key":"22_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Optimality in abstractions of model checking","author":"R. Cleaveland","year":"1995","unstructured":"R. Cleaveland and P. Iyer and D. Yankelevich. Optimality in abstractions of model checking. Proc. SAS\u201995: Proc. 2d. Static Analysis Symposium, Lecture Notes in Computer Science 983, Springer, 1995, 1995."},{"key":"22_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Faster Model Checking for the Modal \u03bc Calculus","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland, M. Klein and B. Steffen. Faster Model Checking for the Modal \u03bc Calculus. Proceedings of the International Workshop on Computer Aided Verification, CAV\u201992, LNCS 663, 1992"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"M. Codish and S. Debray and R. Giacobazzi. Compositional analysis of modular logic programs. Proc. 20th ACM Symp. on Principles of Programming Languages, 1993, pp. 451\u2013464.","DOI":"10.1145\/158511.158703"},{"key":"22_CR12","unstructured":"M. Codish and M. Falaschi and K. Marriott, Suspension analysis for concurrent logic programs. Proc. 8th Int\u2019l. Conf. on Logic Programming, MIT Press, 1991, pp. 331\u2013345."},{"key":"22_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1007\/3-540-09526-8_57","volume-title":"On rational expressions representing infinite rational trees","author":"G. Cousineau","year":"1979","unstructured":"G. Cousineau and M. Nivat. On rational expressions representing infinite rational trees. Proc. 8th Conf. Math. Foundations of Computer Science: MFCS\u201979, Lecture Notes in Computer Science 74, Springer, 1979, pp. 567\u2013580."},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"P. Cousot, R. Cousot. Abstract interpretation: A unified Lattice Model for static Analysis of Programs by Construction or Approximation of Fixpoints. In Proceedings 4th ACM Symp. on Principles of Programming Languages, POPL\u201977, Los Angeles, California, January, 1977","DOI":"10.1145\/512950.512973"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Systematic design of program analysis frameworks. Proc. 6th ACM Symp. on Principles of Programming Languages, POPL\u201979, 1979, pages 269\u2013282.","DOI":"10.1145\/567752.567778"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Inductive Definitions, Semantics, and Abstract Interpretation. Proc. 19th ACM Symp. on Principles of Programming Languages, POPL\u201992, 1992, pp. 83\u201394.","DOI":"10.1145\/143165.143184"},{"key":"22_CR17","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. Journal of Logic and Computation 2 (1992) 511\u2013547.","journal-title":"Journal of Logic and Computation"},{"key":"22_CR18","volume-title":"Ph.D. thesis","author":"D. Dams","year":"1996","unstructured":"D. Dams. Abstract interpretation and partition refinement for model checking. Ph.D. thesis, Technische Universiteit Eindhoven, The Netherlands, 1996."},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"M. Dwyer and L. Clark. Data Flow Analysis for Verifying Properties of Concurrent Programs. Proc. 2d ACM SIGSOFT Symposium on Foundations of Software Engineering, 1994, pp.62\u201375.","DOI":"10.1145\/193173.195295"},{"key":"22_CR20","unstructured":"M. Dwyer and D. Schmidt, Limiting State Explosion with Filter-Based Refinement. Proc. International Workshop on Verification, Model Checking and Abstract Interpretation, Port Jefferson, Long Island, N.Y., http:\/\/www.cis.ksu.edu\/~schmidt\/papers\/filter.ps.Z , 1997."},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"M. Dwyer and C. Pasareanu. Filter-based Model Checking of Partial Systems. Proceedings of the 6th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Orlando, FL, USA, 1998.","DOI":"10.1145\/288195.288307"},{"key":"22_CR22","unstructured":"E. Emerson, J. Lei, Efficient model checking in fragments of the propositional mucalculus. In Proceedings LICS\u201986, 267\u2013278, 1986"},{"key":"22_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/3-540-56610-4_81","volume-title":"Gate splitting in LOTOS specifications using abstract interpretation","author":"F. Giannotti","year":"1993","unstructured":"F. Giannotti and D. Latella, Gate splitting in LOTOS specifications using abstract interpretation. In Proc. TAPSOFT\u201993, M.-C. Gaudel and J.-P. Jouannaud, eds. LNCS 668, Springer, 1993, pp. 437\u2013452."},{"key":"22_CR24","series-title":"Lect Notes Comput Sci","first-page":"417","volume-title":"Using Partial orders for the eficient verification of deadlock freedom and safety properties","author":"P. Godefroid","year":"1992","unstructured":"Godefroid, P. and Wolper, P. Using Partial orders for the eficient verification of deadlock freedom and safety properties. Proc. of the Third Workshop on Computer Aided Verification, Springer-Verlag, LNCS 575, 1991, pp. 417\u2013428."},{"key":"22_CR25","unstructured":"M. Hecht, Flow Analysis of Computer Programs. Elsevier, 1977"},{"key":"22_CR26","unstructured":"N.D. Jones and C. Gomard and P. Sestoft, Partial Evaluation and Automatic Program Generation. Prentice Hall, 1993."},{"key":"22_CR27","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1145\/321921.321938","volume":"23","author":"J. Kam","year":"1976","unstructured":"J. Kam and J. Ullman. Global data flow analysis and iterative algorithms. Journal of the ACM 23 (1976) 158\u2013171.","journal-title":"Journal of the ACM"},{"key":"22_CR28","first-page":"194","volume-title":"A unified approach to global program optimization","author":"G. A. Kildall","year":"1973","unstructured":"G. A. Kildall. A unified approach to global program optimization. In Conf. Rec. 1st ACM Symposium on Principles of Programming Languages (POPL\u201973), pages 194\u2013206. ACM, New York, 1973."},{"key":"22_CR29","series-title":"Lect Notes Comput Sci","volume-title":"Parallelism for Free: Bitvector Analysis-No State explosion!","author":"J. Knoop","year":"1995","unstructured":"J. Knoop, B. Steffen and J. Vollmer Parallelism for Free: Bitvector Analysis-No State explosion! Proceedings of the International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201995, LNCS 1019, 1995"},{"key":"22_CR30","unstructured":"J. Knoop, O. R\u00fcthing and B. Steffen. Lazy Code Motion. Proceedings of the ACM SIGPLAN\u201994 Conference on Programming Language Design and Implementation (PLDI\u201994), Olando, Florida, SIPLAN Notices 30, 6 (1994), 233\u2013245."},{"key":"22_CR31","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen, Results on the propositional mu-calculus. Theoretical Computer Science, 27 (1983) 333\u2013354.","journal-title":"Theoretical Computer Science"},{"key":"22_CR32","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0304-3975(77)90041-X","volume":"5","author":"Y.S. Kwong","year":"1977","unstructured":"Y.S. Kwong, On reduction of asynchronous systems. Theoretical Computer Science 5 (1977) 25\u201350.","journal-title":"Theoretical Computer Science"},{"key":"22_CR33","unstructured":"S.P. Masticola and B.G. Ryder. Static Infinite Wait Anomaly Detection in Polynomial Time. Proceedings of ACM International Conference on Parallel Processing, 1990."},{"key":"22_CR34","doi-asserted-by":"crossref","unstructured":"S.P. Masticola and B.G. Ryder. A Model of Ada Programs for Static Deadlock Detection in Polynomial Time. Proceedings ACM Workshop on Parallel and Distributed Debugging, 1991.","DOI":"10.1145\/122759.122768"},{"key":"22_CR35","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, 1989."},{"key":"22_CR36","first-page":"209","volume":"17","author":"R. Milner","year":"1992","unstructured":"R. Milner and M. Tofte. Co-induction in relational semantics. Theoretical Computer Science, 17 (1992) 209\u2013220.","journal-title":"Theoretical Computer Science"},{"key":"22_CR37","series-title":"Lect Notes Comput Sci","first-page":"156","volume-title":"Programs as Data Objects","author":"A. Mycroft","year":"1985","unstructured":"A. Mycroft and N.D. Jones. A relational framework for abstract interpretation. In Programs as Data Objects, Lecture Notes in Computer Science 217, Springer, 1985, pp. 156\u2013171."},{"key":"22_CR38","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BF00263194","volume":"18","author":"F. Nielson","year":"1982","unstructured":"F. Nielson, A Denotational Framework for Data Flow Analysis. Acta Informatica 18 (1982) 265\u2013287.","journal-title":"Acta Informatica"},{"key":"22_CR39","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1109\/32.48935","volume":"16-3","author":"K.M. Olender","year":"1990","unstructured":"K.M. Olender and L.J. Osterweil. Cecil: A Sequencing Constraint Language for Automatic Static Analysis Generation. IEEE Transactions on Software Engineering 16-3 (1990) 268\u2013280.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"22_CR40","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/125489.122822","volume":"1-1","author":"K.M. Olender","year":"1992","unstructured":"K.M. Olender and L.J. Osterweil. Interprocedural Static Analysis of Sequencing Constraints. ACM Transactions on Software Engineering and Methodology 1-1 (1992) 21\u201352.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"22_CR41","series-title":"Technical Report","volume-title":"A Structural Approach to Operational Semantics","author":"G. D. Plotkin","year":"1981","unstructured":"Gordon D. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, University of Aarhus, Denmark, 1981."},{"key":"22_CR42","doi-asserted-by":"crossref","unstructured":"D.A. Schmidt, Abstract interpretation of small-step semantics. Proc. 5th LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages, M. Dam and F. Orava, eds. Springer, 1996.","DOI":"10.1007\/3-540-62503-8_4"},{"key":"22_CR43","first-page":"237","volume":"10","author":"D.A. Schmidt","year":"1998","unstructured":"D.A. Schmidt, Trace-based abstract interpretation of operational semantics. J. Lisp and Symbolic Computation, 10 (1998) 237\u2013271.","journal-title":"Trace-based abstract interpretation of operational semantics. J. Lisp and Symbolic Computation"},{"key":"22_CR44","doi-asserted-by":"crossref","unstructured":"D.A. Schmidt, Data-flow analysis is model checking of abstract interpretations. Proc. 25th ACM Symp. on Principles of Prog. Languages, POPL98, 1998.","DOI":"10.1145\/268946.268950"},{"key":"22_CR45","series-title":"LFCS report","volume-title":"Ph.D. thesis","author":"F. Silva da","year":"1992","unstructured":"F. daSilva. Correctness Proofs of Compilers and Debuggers: an Approach Based on Structural Operational Semantics. Ph.D. thesis, LFCS report ECS-LFCS-92-241, Edinburgh University, Scotland, 1992."},{"key":"22_CR46","doi-asserted-by":"crossref","unstructured":"B. Steffen, T. Margaria, V. Braun: The Electronic Tool Integration platform: concepts and design, [51] 1(1), pp. 9\u201330.","DOI":"10.1007\/s100090050003"},{"key":"22_CR47","series-title":"Lect Notes Comput Sci","volume-title":"Data Flow Analysis as Model Checking","author":"B. Steffen","year":"1991","unstructured":"B. Steffen. Data Flow Analysis as Model Checking. Proceedings of the International Concerence on Theoretical Aspects of Computer Software, TACS\u201991, LNCS 526, 1991"},{"key":"22_CR48","doi-asserted-by":"crossref","unstructured":"B. Steffen. Generating Data Flow Analysis Algorithms from Modal Specifications, International Journal on Science of Computer Programming, N. 21, 1993, pp. 115\u2013139.","DOI":"10.1016\/0167-6423(93)90003-8"},{"key":"22_CR49","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/3-540-61739-6_31","volume-title":"Property-oriented expansion","author":"B. Steffen","year":"1996","unstructured":"B. Steffen, Property-oriented expansion. Proc. Static Analysis Symposium: SAS\u201996, Lecture Notes in Computer Science 1145. Springer, 1996, pp. 22\u201341."},{"key":"22_CR50","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Unifying Models","author":"B. Steffen","year":"1997","unstructured":"B. Steffen, Unifying Models. Proc. of the Annual Symposium on Theoretical Aspects of Computer Science, STACS\u201997, Lecture Notes in Computer Science 1200. Springer, 1997, pp. 1\u201320."},{"key":"22_CR51","unstructured":"Special Section on Programming Language Tools, Int. Journal on Software Tools for Technology Transfer, Vol. 3, Springer Verlag, October 1998"},{"key":"22_CR52","series-title":"Lect Notes Comput Sci","volume-title":"Abstract interpretation of the pi-calculus","author":"A. Venet","year":"1996","unstructured":"A. Venet, Abstract interpretation of the pi-calculus. Proc. LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages, M. Dam and F. Orava, eds., LNCS 1192, Springer, 1996."},{"key":"22_CR53","series-title":"Lect Notes Comput Sci","volume-title":"Automatic Determination of Communication Topologies in Mobile Systems","author":"A. Venet","year":"1998","unstructured":"A. Venet, Automatic Determination of Communication Topologies in Mobile Systems. Proc. SAS\u201998, G. Levi, ed. Springer LNCS, 1998."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49727-7_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T15:46:22Z","timestamp":1556466382000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49727-7_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540650140","9783540497271"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/3-540-49727-7_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}