{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T11:06:24Z","timestamp":1742382384332},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540617396"},{"type":"electronic","value":"9783540706748"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61739-6_31","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:19:26Z","timestamp":1330294766000},"page":"22-41","source":"Crossref","is-referenced-by-count":30,"title":["Property-oriented expansion"],"prefix":"10.1007","author":[{"given":"Bernhard","family":"Steffen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"3_CR1","unstructured":"A.V. Aho, R. Sethi, J.D. Ullman. Compilers: Principles, Techniques and Tools, Addison-Wesley, 1985."},{"key":"3_CR2","unstructured":"J. Bradfield, C.Stirling. Local Model Checking for Infinite State Spaces. LFCS Report Series ECS-LFCS-90-115, June 1990"},{"key":"3_CR3","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":"3_CR4","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/201059.201061","volume":"17","author":"C. Click","year":"1995","unstructured":"C. Click, K.D. Cooper. Combining Anlyses, Combining Optimizations, ACM TOPLAS N.2, Vol.17, pp.181\u2013196, 1995","journal-title":"ACM TOPLAS N.2"},{"key":"3_CR5","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":"3_CR6","volume-title":"Ph.D. Thesis","author":"C. Click","year":"1995","unstructured":"C. Click. Combining Analyses, Combining Optimizations, Ph.D. Thesis, Rice University, Houston, TX, 1995, 149 pages."},{"key":"3_CR7","unstructured":"E. Emerson, J. Lei, Efficient model checking in fragments of the propositional mu-calculus. In Proceedings LICS'86, 267\u2013278, 1986"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"R. Giegerich, U. M\u00f6ncke, R. Wilhelm. Invariance of Approximative Semantics with Respect to Program Transformations, Informatik-Fachberichte 50, pp. 1\u201310, Proc. of the third Conference of the European Co-operation in Informatics, Springer, 1981.","DOI":"10.1007\/978-3-662-01089-1_1"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"P. Godefroit. Partial-Order Methods for the Verification of Concurrent Systems. LNCS Monography, LNCS 1032, 1996.","DOI":"10.1007\/3-540-60761-7"},{"key":"3_CR10","doi-asserted-by":"crossref","first-page":"679","DOI":"10.1007\/BF00282621","volume":"24","author":"S. Horwitz","year":"1987","unstructured":"S. Horwitz, A. Demers, T. Teitelbaum. An Efficient General Iterative Algorithm for Data Flow Analysis, Acta Informatica, vol. 24, pp. 679\u2013694, 1987.","journal-title":"Acta Informatica"},{"key":"3_CR11","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'73), pages 194\u2013206. ACM, New York, 1973."},{"key":"3_CR12","unstructured":"M. Klein, J. Knoop, D. Kosch\u00fctzki, B. Steffen. DFA & OPT-MetaFrame: A Toolkit for Program Analysis and Optimization (Tool description) \u2014 Proc. TACAS'96, Int. Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Passau, LNCS 1055 Springer, pp. 418\u2013421"},{"key":"3_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":"3_CR14","doi-asserted-by":"crossref","unstructured":"J. Knoop, O. R\u00fcthing, B. Steffen. Partial Dead Code Elimination, SIGPLAN PLDI Conference'94, ACM SIGPLAN Notices 29, Orlando, June 1994","DOI":"10.1145\/178243.178256"},{"issue":"6","key":"3_CR15","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/223428.207150","volume":"30","author":"J. Knoop","year":"1995","unstructured":"J. Knoop, O. R\u00fcthing, B. Steffen. The Power of Assignment Motion, Proc. of the ACM SIGPLAN'95 Conference on Programming Language Design and Implemantion (PLDI'95), La Jolla, California, June 1995, SIGPLAN Notices 30, 6 (1995), 233\u2013245","journal-title":"SIGPLAN Notices"},{"issue":"N.1","key":"3_CR16","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z. Manna","year":"1984","unstructured":"Z. Manna, P. Wolper. \u201cSynthesis of Communicating Processes from Temporal Logic Specifications,\u221d ACM TOPLAS Vol.6, N.1, Jan. 1984, pp.68\u201393.","journal-title":"ACM TOPLAS"},{"key":"3_CR17","doi-asserted-by":"publisher","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. Communications of the ACM 22, 96\u2013103, 1979","journal-title":"Communications of the ACM"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"N.D. Jones, F. Nielson. Abstract Interpretation: A Semantics-Based Tool for Program Analysis. In Handbook of Logics in Computer Science, Vol. 4, pp. 527\u2013637, Oxford University Press, 1995.","DOI":"10.1093\/oso\/9780198537809.003.0005"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"B.K. Rosen, M.N. Wegman, F.K. Zadeck. \u201cGlobal Value Numbers and Redundant Computations\u221d. 15th POPL, San Diego, California, 12\u201327, 1988","DOI":"10.1145\/73560.73562"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"B. Steffen, A.Ingolfsdottir. Characteristic Formulae for Finite State Processes, International Journal on Information and Computation, Vol. 110, No. 1, 1994","DOI":"10.1006\/inco.1994.1028"},{"issue":"N.3","key":"3_CR21","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"A.P. Sistla, E.M. Clarke. \u201cThe Complexity of the Propositional Linear Temporal Logics,\u221d Journal of the ACM, Vol.32, N.3, July 1985, pp.733\u2013749.","journal-title":"Journal of the ACM"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"B. Steffen. Characteristic Formulae. Proceedings of the International Colloquium on Automata, Languages and Programming, ICALP'89, LNCS 372, 1989","DOI":"10.1007\/BFb0035794"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"B. Steffen. Data Flow Analysis as Model Checking. Proceedings of the International Concerence on Theoretical Aspects of Computer Software, TACS'91, LNCS 526, 1991","DOI":"10.1007\/3-540-54415-1_54"},{"key":"3_CR24","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0167-6423(93)90003-8","volume":"N. 21","author":"B. Steffen","year":"1993","unstructured":"B. Steffen. Generating Data Flow Analysis Algorithms from Modal Specifications, International Journal on Science of Computer Programming, N. 21, 1993, pp. 115\u2013139.","journal-title":"International Journal on Science of Computer Programming"},{"key":"3_CR25","unstructured":"B. Steffen, T. Margaria, A. Cla\u00dfen. Heterogeneous Analysis and Verification for Distributed Systems, In \u201cSOFTWARE: Concepts and Tools\u221d, vol. 17, N.1, pp. 13\u201325, Springer Verlag, 1996."},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"A. Tarski. A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics, v. 5, 1955.","DOI":"10.2140\/pjm.1955.5.285"},{"issue":"3","key":"3_CR27","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/99164.99179","volume":"25","author":"D. Whitfield","year":"1990","unstructured":"D. Whitfield, M.L. Soffa. An Approach to Ordering Optimizing Transformations, Proc. 2nd ACM SIGPLAN Symposium on Principles & Practice of Parallel Programming (PPOPP), Seattle, Washington, SIGPLAN Notes 25,3, pp.137\u2013147, March 1990.","journal-title":"SIGPLAN Notes"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61739-6_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:44:22Z","timestamp":1713635062000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61739-6_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617396","9783540706748"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-61739-6_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}