{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:59:28Z","timestamp":1725663568446},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540572640"},{"type":"electronic","value":"9783540480273"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-57264-3_29","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:34:11Z","timestamp":1330259651000},"page":"60-71","source":"Crossref","is-referenced-by-count":0,"title":["Abstract interpretation and verification of reactive systems"],"prefix":"10.1007","author":[{"given":"J. C.","family":"Fernandez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, S. Bensalem, C. Loiseaux, and J. Sifakis. Property preserving simulations. In Workshop on Computer-Aided Verification (CAV), Montr\u00e9al, page, To appear LNCS, June 1992.","DOI":"10.1007\/3-540-56496-9_21"},{"key":"5_CR2","unstructured":"J.R. Burch, E.M. Clarke, K.L McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th IEEE,LICS, 1990."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"A. Bouali and R. de Simone. Symbolic bisimulation minimisation. In Fourth Workshop on Computer-Aided Verification,Montreal, june 1992.","DOI":"10.1007\/3-540-56496-9_9"},{"key":"5_CR4","unstructured":"A. Bouajjani, J.C. Fernandez, and N. Halbwachs. Minimal model generation. In Workshop on Computer-aided Verification, Rutgers, American Mathematical Society, Association for Computing Machinery, June 1990."},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J.C. Fernandez, N. Halbwachs, C. Ratel, and P. Raymond. Minimal state graph generation. Science of Computer Programming, 18(3), June 1992.","DOI":"10.1016\/0167-6423(92)90018-7"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In International Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407, Springer Verlag, 1989.","DOI":"10.1007\/3-540-52148-8_30"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In 2th Int. Symp. on Programming, pages 106, 130, Dunod, 1976.","DOI":"10.1145\/390018.808314"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th POPL, January 1977.","DOI":"10.1145\/512950.512973"},{"key":"5_CR10","unstructured":"P. Cousot and R. Cousot. Comparing the Galois Connectionn and Widening\/Narrowing Approaches to Abstract Interpretation. Technical Report, LIX, Ecole Polytechnique, May 1990."},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In 5th. Annual Symp. on Principles of Programming Languages, pages 84\u201387, 1977.","DOI":"10.1145\/512760.512770"},{"key":"5_CR12","volume-title":"Semantic Foundations of Program Analysis","author":"P. Cousot","year":"1981","unstructured":"P. Cousot. Semantic Foundations of Program Analysis, chapter 10. Prentice Hall, Inc., Englewood Cliffs, 1981."},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"R. Enders, T. Filkorn, and D. Taubner. Generating bdds for symbolic model checking in ccs. In K. G. Larsen, editor, Proceedings of the 3rd Workshop on Computer-Aided Verification (Aalborg, Denmark), july 1\u20134 1991.","DOI":"10.1007\/3-540-55179-4_20"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"J. C. Fernandez. An implementation of an efficient algorithm for bisimulation equivalence. Science of Computer Programming, 13(2\u20133), May 1990.","DOI":"10.1016\/0167-6423(90)90071-K"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"J. Cl. Fernandez, A. Kerbrat, and L. Mounier. Symbolic equivalence checking. In Workshop on Computer-aided Verification, University of Crete, to appear, July 1993.","DOI":"10.1007\/3-540-56922-7_8"},{"key":"5_CR16","unstructured":"J.Cl. Fernandez and L. Mounier. A tool set for deciding behavioural equivalences. In J.F. Groote J.C.M. Baeten, editor, CONCUR'91, Concurrency theory, LNCS 527, Springer Verlag, August 26\u201329 1991."},{"key":"5_CR17","volume-title":"CS-R 8911","author":"R.J. Glabbeek Van","year":"1989","unstructured":"R.J. Van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics (extended abstract). CS-R 8911, Centrum voor Wiskunde en Informatica, Amsterdam, 1989."},{"key":"5_CR18","unstructured":"N. Halbwachs. D\u00e9termination Automatique de Relations Lin\u00e9aires V\u00e9rifi\u00e9es par les Variables d'un Programme. PhD thesis, Universit\u00e9 de Grenoble, 1979."},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, P. Raymond, and C. Ratel. Generating efficient code from dataflow programs. In Third International Symposium on Programming Language Implementation and Logic Programming, Passau, August 1991.","DOI":"10.1007\/3-540-54444-5_100"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"P. Kanellakis and S. Smolka. Ccs expressions, finite state processes and three problems of equivalence. Information and Computation, 86(1), May 1990.","DOI":"10.1016\/0890-5401(90)90025-D"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"R. Milner. A calculus of communication systems. In LNCS 92, Springer Verlag, 1980.","DOI":"10.1007\/3-540-10235-3"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"D. Park. Concurrency and automata on infinite sequences. In 5th GI-Conference on Theorical Computer Science, Springer Verlag, 1981. LNCS 104.","DOI":"10.1007\/BFb0017309"},{"issue":"nr4","key":"5_CR23","first-page":"339","volume":"11","author":"L. E. Sanchis","year":"1977","unstructured":"Luis E. Sanchis. Data types as lattices: retractions, projection and projection. In RAIRO Theorical computer science, vol 11, nr 4, pages 339\u2013344, 1977.","journal-title":"RAIRO Theorical computer science"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"J. Sifakis. A unified approach for studying the properties of transition systems. TCS, 18, 1982.","DOI":"10.1016\/0304-3975(82)90067-6"},{"key":"5_CR25","volume-title":"4th Workshop on Logics of Programs","author":"J. Sifakis","year":"1983","unstructured":"J. Sifakis. Property preserving homomorphisms of transition systems. In 4th Workshop on Logics of Programs, Pittsburgh, LNCS 164, Springer Verlag, June 1983."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57264-3_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T18:30:26Z","timestamp":1687285826000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57264-3_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540572640","9783540480273"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-57264-3_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}