{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T23:10:08Z","timestamp":1762297808058},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544159"},{"type":"electronic","value":"9783540476177"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54415-1_54","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:46:01Z","timestamp":1330209961000},"page":"346-364","source":"Crossref","is-referenced-by-count":72,"title":["Data flow analysis as model checking"],"prefix":"10.1007","author":[{"given":"Bernhard","family":"Steffen","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"17_CR1","unstructured":"J. Bradfield, C.Stirling. Local Model Checking for Finite State Spaces. LFCS Report Series ECS-LFCS-90-115, June 1990"},{"key":"17_CR2","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 POPL, Los Angeles, California, January, 1977","DOI":"10.1145\/512950.512973"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"E. Clarke, E.A. Emerson, A.P. Sistla. Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications: A Practical Approach. In Proceedings 10th POPL'83, 1983","DOI":"10.1145\/567067.567080"},{"key":"17_CR4","unstructured":"R. Cleaveland, J.G. Parrow, B. Steffen. A Semantic-Based Verification Tool for Finite-State-Systems. Protocol Specification, Testing and Verification, IX, Elsevier Science Publications B.V. (North Holland), 287\u2013302, 1990"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, J.G. Parrow, B. Steffen. The Concurrency Workbench. Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407, 1989","DOI":"10.1007\/3-540-52148-8_3"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, B. Steffen. Computing Behavioural Relations, Logically. In Proceedings ICALP'91, LNCS, 1991","DOI":"10.1007\/3-540-54233-7_129"},{"key":"17_CR7","unstructured":"R. Cleaveland, B. Steffen. A Linear-Time Model-Checking Alogorithm for the Alternation-Free Modal Mu-Calculus. In Proceedings CAV'91"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"D. Dhamdhere. A Fast Algorithm for Code Movement Optimization. SIGPLAN Notices, Vol. 23, 1988","DOI":"10.1145\/51607.51621"},{"key":"17_CR9","unstructured":"E. Emerson, J. Lei, Efficient model checking in fragments of the propositional mu-calculus. In Proceedings LICS'86, 267\u2013278, 1986"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"R. Giegerich. Automatic Generation of Machine Specific Code Generation. In Proceedings 9th POPL, Albuquerque, New Mexico, January, 1982","DOI":"10.1145\/582153.582162"},{"key":"17_CR11","volume-title":"Flow Analysis of Computer Programs","author":"S.M. Hecht","year":"1977","unstructured":"S.M. Hecht Flow Analysis of Computer Programs. Elsevier, North Holland, 1977"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"G.A. Kildall. A Unified Approach to Global Program Optimization. In Proceedings 1st POPL, Boston, Massachusetts, 194\u2013206, 1973","DOI":"10.1145\/512927.512945"},{"key":"17_CR13","doi-asserted-by":"crossref","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. TCS 27, 333\u2013354, 1983","journal-title":"TCS"},{"key":"17_CR14","unstructured":"K. Larsen. Proof Systems for Hennessy-Milner Logic with Recursion, in Proceedings CAAP 1988."},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"P.D. Mosses. Action Semantics. To appear 1991","DOI":"10.1017\/CBO9780511569869"},{"key":"17_CR16","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1145\/359060.359069","volume":"22","author":"E. Morel","year":"1979","unstructured":"E. Morel, C. Renvoise. Global Optimization by Suppression of Partial Redundancies. CACM 22, 96\u2013103, 1979","journal-title":"CACM"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"P.D. Mosses, A.A. Watt. The Use of Action Semantics. In Formal Description of Programming Concepts \u2014 III, 1986","DOI":"10.7146\/dpb.v15i217.7568"},{"key":"17_CR18","first-page":"31","volume":"21","author":"F. Nielson","year":"1986","unstructured":"F. Nielson. A Bibliography on Abstract Interpretations. ACM SIGPLAN Notices 21, 31\u201338, 1986","journal-title":"ACM SIGPLAN Notices"},{"key":"17_CR19","doi-asserted-by":"crossref","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, 265\u2013287, 1982","journal-title":"Acta Informatica"},{"key":"17_CR20","unstructured":"G. Plotkin. A Structural Approach to Operational Semantics. University of Aarhus, DAIMI FN-19, 1981"},{"issue":"2","key":"17_CR21","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1145\/64140.65006","volume":"24","author":"P. Lee","year":"1989","unstructured":"Peter Lee, Frank Pfenning, Gene Rollins, and William Scherlis. The Ergo Support System: An Integrated Set of Tools for Prototyping Integrated Environments. SIGPLAN Notices, Vol. 24, No. 2, 25\u201334, February 1989","journal-title":"SIGPLAN Notices"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"B. K. Rosen, M. N. Wegman and F. K. Zadeck. \u201cGlobal Value Numbers and Redundant Computations\u201d. 15th POPL, San Diego, California, 12\u201327, 1988","DOI":"10.1145\/73560.73562"},{"key":"17_CR23","unstructured":"S. Sagiv, N. Francez, M. Rodeh, R. Wilhelm. A Logic-Based Approach to Data Flow Analysis Problems. To appear 1990"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"B. Steffen, J. Knoop, O. R\u00fcthing. The Value Flow Graph: A Program Representation for Optimal Program Transformations. In Proceedings ESOP'90, LNCS 432, 1990","DOI":"10.1007\/3-540-52592-0_76"},{"key":"17_CR25","unstructured":"B. Steffen, J. Knoop, O. R\u00fcthing. Optimal Placement of Computations within Flow Graphs: A Practical Approach. In Proceedings TAPSOFT'91, LNCS, 1991"},{"key":"17_CR26","volume-title":"Program Flow Analysis: Theory and Applications","author":"M. Sharir","year":"1981","unstructured":"M. Sharir, A. Pnueli. Two Approaches to Interprocedural Data Flow Analysis. In: S.S. Muchnick, N.D. Jones. Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs, N.J., 1981"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"B. Steffen. Characteristic Formulae. In Proceedings ICALP'89, LNCS 372, 1989","DOI":"10.1007\/BFb0035794"},{"key":"17_CR28","unstructured":"B. Steffen. Generating Data Flow Analysis Algorithms from Modal Specifications. Technical Report of the RWTH-Aachen, to appear 1991"},{"key":"17_CR29","unstructured":"C. Stirling. Modal and Temporal Logics. In Handbook of Logics in Computer Science, Vol. 1, Oxford University Press, to appear 1990."},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Tarski, A. \u201cA Lattice-Theoretical Fixpoint Theorem and its Applications.\u201d Pacific Journal of Mathematics, v. 5, 1955.","DOI":"10.2140\/pjm.1955.5.285"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"G. A. Venkatesh. A framework for construction and evaluation of high-level specifications for program analysis techniques. In Proceedings SIGPLAN'89, 1989","DOI":"10.1145\/73141.74819"},{"key":"17_CR32","volume-title":"Program Flow Analysis: Theory and Applications","author":"R. Wilhelm","year":"1981","unstructured":"R. Wilhelm. Global Flow Analysis and Optimization in the MUG2 Compiler Generating System. In: S.S. Muchnick, N.D. Jones. Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs, N.J., 1981"},{"key":"17_CR33","first-page":"257","volume":"26","author":"R. Wilhelm","year":"1974","unstructured":"R. Wilhelm. Codeoptimierung mittels attributierter Transformationsgrammatiken. LNCS 26, 257\u2013266, 1974","journal-title":"LNCS"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54415-1_54.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:21:26Z","timestamp":1619572886000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54415-1_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544159","9783540476177"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-54415-1_54","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}