{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T14:06:54Z","timestamp":1751983614720},"reference-count":36,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[1993,10,1]],"date-time":"1993-10-01T00:00:00Z","timestamp":749433600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":7229,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[1993,10]]},"DOI":"10.1016\/0167-6423(93)90003-8","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T00:09:22Z","timestamp":1027642162000},"page":"115-139","source":"Crossref","is-referenced-by-count":61,"title":["Generating data flow analysis algorithms from modal specifications"],"prefix":"10.1016","volume":"21","author":[{"given":"Bernhard","family":"Steffen","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0167-6423(93)90003-8_BIB1","article-title":"Local model checking for infinite state spaces","author":"Bradfield","year":"1990","journal-title":"LFCS Report Series ECS-LFCS-90-115"},{"key":"10.1016\/0167-6423(93)90003-8_BIB2","doi-asserted-by":"crossref","DOI":"10.1145\/567067.567080","article-title":"Automatic verification of finite state concurrent systems using temporal logic specifications: a practical approach","author":"Clarke","year":"1983","journal-title":"Proceedings 10th POPL'83"},{"key":"10.1016\/0167-6423(93)90003-8_BIB3","doi-asserted-by":"crossref","DOI":"10.1145\/151646.151648","article-title":"The concurrency workbench: a semantics-based verification tool for finite state systems","author":"Cleaveland","year":"1993","journal-title":"ACM Trans. Programming Languages Syst."},{"key":"10.1016\/0167-6423(93)90003-8_BIB4","first-page":"287","article-title":"A semantic-based verification tool for finite-state-systems","volume":"IX","author":"Cleaveland","year":"1990"},{"key":"10.1016\/0167-6423(93)90003-8_BIB5","article-title":"Computing behavioural relations, logically","volume":"501","author":"Cleaveland","year":"1991"},{"key":"10.1016\/0167-6423(93)90003-8_BIB6","article-title":"A linear-time model-checking algorithm for the alternation-free modal mu-calculus","volume":"575","author":"Cleaveland","year":"1991"},{"key":"10.1016\/0167-6423(93)90003-8_BIB7","article-title":"Faster model checking for the modal mu-calculus","volume":"663","author":"Cleaveland","year":"1992"},{"key":"10.1016\/0167-6423(93)90003-8_BIB8","article-title":"Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints","author":"Cousot","year":"1977","journal-title":"Proceedings 4th POPL"},{"key":"10.1016\/0167-6423(93)90003-8_BIB9","doi-asserted-by":"crossref","DOI":"10.1145\/51607.51621","article-title":"A fast algorithm for code movement optimization","volume":"23","author":"Dhamdhere","year":"1988","journal-title":"SIGPLAN Notices"},{"key":"10.1016\/0167-6423(93)90003-8_BIB10","first-page":"267","article-title":"Efficient model checking in fragments of the propositional mu-calculus","author":"Emerson","year":"1986","journal-title":"Proceedings LICS'86"},{"key":"10.1016\/0167-6423(93)90003-8_BIB11","article-title":"Automatic generation of machine specific code generation","author":"Giegerich","year":"1982","journal-title":"Proceedings 9th POPL"},{"key":"10.1016\/0167-6423(93)90003-8_BIB12","series-title":"Flow Analysis of Computer Programs","author":"Hecht","year":"1977"},{"key":"10.1016\/0167-6423(93)90003-8_BIB13","first-page":"194","article-title":"A unified approach to global program optimization","author":"Kildall","year":"1973","journal-title":"Proceedings 1st POPL"},{"issue":"7","key":"10.1016\/0167-6423(93)90003-8_BIB14","article-title":"Proceedings ACM SIGPLAN'92 Conference on Programming Language Design and Implementation","volume":"27","author":"Knoop","year":"1992","journal-title":"SIGPLAN Notices"},{"key":"10.1016\/0167-6423(93)90003-8_BIB15","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional mu-calculus","volume":"27","author":"Kozen","year":"1983","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0167-6423(93)90003-8_BIB16","article-title":"Proof systems for Hennessy\u2013Milner logic with recursion","volume":"299","author":"Larsen","year":"1988"},{"key":"10.1016\/0167-6423(93)90003-8_BIB17","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1145\/64140.65006","article-title":"The ergo support system: an integrated set of tools for prototyping integrated environments","volume":"24","author":"Lee","year":"1989","journal-title":"SIGPLAN Notices"},{"key":"10.1016\/0167-6423(93)90003-8_BIB18","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1145\/359060.359069","article-title":"Global optimization by suppression of partial redundancies","volume":"22","author":"Morel","year":"1979","journal-title":"Comm. ACM"},{"key":"10.1016\/0167-6423(93)90003-8_BIB19","article-title":"Action semantics","volume":"26","author":"Mosses","year":"1992","journal-title":"Cambridge Tracts Theoret. Comput. Sci."},{"key":"10.1016\/0167-6423(93)90003-8_BIB20","article-title":"The use of action semantics","volume":"III","author":"Mosses","year":"1986","journal-title":"Formal Description of Programming Concepts"},{"key":"10.1016\/0167-6423(93)90003-8_BIB21","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 Inform."},{"key":"10.1016\/0167-6423(93)90003-8_BIB22","first-page":"31","article-title":"A bibliography on abstract interpretations","volume":"21","author":"Nielson","year":"1986","journal-title":"ACM SIGPLAN Notices"},{"key":"10.1016\/0167-6423(93)90003-8_BIB23","series-title":"DAIMI FN-19","article-title":"A structural approach to operational semantics","author":"Plotkin","year":"1981"},{"key":"10.1016\/0167-6423(93)90003-8_BIB24","article-title":"Global value numbers and redundant computations","author":"Rosen","year":"1988","journal-title":"Proceedings 15th POPL"},{"key":"10.1016\/0167-6423(93)90003-8_BIB25","unstructured":"S. Sagiv, N. Francez, M. Rodeh and R. Wilhelm, A logic-based approach to data flow analysis problems (to appear)."},{"key":"10.1016\/0167-6423(93)90003-8_BIB26","series-title":"Program Flow Analysis: Theory and Applications","article-title":"Two approaches to interprocedural data flow analysis","author":"Sharir","year":"1981"},{"key":"10.1016\/0167-6423(93)90003-8_BIB27","article-title":"Characteristic formulae","volume":"372","author":"Steffen","year":"1989"},{"key":"10.1016\/0167-6423(93)90003-8_BIB28","article-title":"Data flow analysis as model checking","volume":"526","author":"Steffen","year":"1991"},{"key":"10.1016\/0167-6423(93)90003-8_BIB29","article-title":"The value flow graph: a program representation for optimal program transformations","volume":"432","author":"Steffen","year":"1990"},{"key":"10.1016\/0167-6423(93)90003-8_BIB30","article-title":"Optimal placement of computations within flow graphs: a practical approach","volume":"494","author":"Steffen","year":"1991"},{"key":"10.1016\/0167-6423(93)90003-8_BIB31","unstructured":"C. Stirling, Modal and temporal logics, in: Handbook of Logics in Computer Science, Vol. 1 (Oxford University Press, Oxford, to appear)."},{"key":"10.1016\/0167-6423(93)90003-8_BIB32","doi-asserted-by":"crossref","DOI":"10.2140\/pjm.1955.5.285","article-title":"A lattice-theoretical fixpoint theorem and its applications","volume":"5","author":"Tarski","year":"1955","journal-title":"Pacific J. Math."},{"key":"10.1016\/0167-6423(93)90003-8_BIB33","doi-asserted-by":"crossref","DOI":"10.1145\/74818.74819","article-title":"A framework for construction and evaluation of high-level specifications for program analysis techniques","author":"Venkatesh","year":"1989","journal-title":"Proceedings SIGPLAN'89"},{"key":"10.1016\/0167-6423(93)90003-8_BIB34","first-page":"257","article-title":"Codeoptimierung mittles attributierter Transformationsgrammatiken","volume":"26","author":"Wilhelm","year":"1974"},{"key":"10.1016\/0167-6423(93)90003-8_BIB35","series-title":"Program Flow Analysis: Theory and Applications","article-title":"Global flow analysis and optimization in the MUG2 compiler generating system","author":"Wilhelm","year":"1981"},{"key":"10.1016\/0167-6423(93)90003-8_BIB36","article-title":"Automatic generation of global optimizers","author":"Whitfield","year":"1991","journal-title":"Proceedings ACM SIGPLAN'91 Conference on Programming Language Design and Implementation"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0167642393900038?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0167642393900038?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,12]],"date-time":"2019-04-12T13:55:22Z","timestamp":1555077322000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0167642393900038"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,10]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1993,10]]}},"alternative-id":["0167642393900038"],"URL":"https:\/\/doi.org\/10.1016\/0167-6423(93)90003-8","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[1993,10]]}}}