{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:32:46Z","timestamp":1761611566640},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439165"},{"type":"electronic","value":"9783540456100"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45610-4_15","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T06:47:11Z","timestamp":1186901231000},"page":"207-221","source":"Crossref","is-referenced-by-count":0,"title":["Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae"],"prefix":"10.1007","author":[{"given":"David","family":"D\u00e9harbe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anamaria Martins","family":"Moreira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christophe","family":"Ringeissen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"15_CR1","unstructured":"NuSMV home page. http:\/\/nusmv.irst.itc.it , accessed on Apr. 23 2002."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems, pages 193\u2013207, 1999.","DOI":"10.21236\/ADA360973"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"P. Borovansk\u00fd, C. Kirchner, H. Kirchner, P.-E. Moreau, and C. Ringeissen. An Overview of ELAN. In C. Kirchner and H. Kirchner, editors, Proc. Second Intl. Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science, Pont-\u00e0-Mousson (France), Sept. 1998. Elsevier.","DOI":"10.1016\/S1571-0661(05)82552-6"},{"key":"15_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs: Workshop","author":"E. Clarke","year":"1981","unstructured":"E. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons for branching time temporal logic. In Logics of Programs: Workshop, volume 131 of LNCS, pages 52\u201371. Springer Verlag, 1981."},{"key":"15_CR5","unstructured":"E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press."},{"key":"15_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/3-540-48119-2_17","volume-title":"World Congress on Formal Methods and their Application(FM\u201999)","author":"D. D\u00e9harbe","year":"1999","unstructured":"D. D\u00e9harbe and A. M. Moreira. Symbolic model checking with fewer fixpoint computations. In World Congress on Formal Methods and their Application(FM\u201999), volume 1708 of LNCS, pages 272\u2013288, 1999."},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In Handbook of Theorectical Computer Science, chapter 15. Elsevier Science Publishers B.V., 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications for finite-state verification. Technical Report UM-CS-1998-035, 1998.","DOI":"10.1145\/298595.298598"},{"key":"15_CR9","series-title":"PhD thesis","volume-title":"Logique du temps arborescent pour la sp\u00e9cification et preuve de programmes","author":"S. Graf","year":"1984","unstructured":"S. Graf. Logique du temps arborescent pour la sp\u00e9cification et preuve de programmes. PhD thesis, Institut National Polytechnique de Grenoble, France, 1984."},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"H. Iwashita, T. Nakata, and F. Hirose. CTL model checking based on forward state traversal. In ICCAD\u201996, page 82, 1996.","DOI":"10.1109\/ICCAD.1996.569084"},{"issue":"4","key":"15_CR11","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15(4):1155\u20131194, 1986.","journal-title":"SIAM Journal on Computing"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton Univ Pr, 1995.","DOI":"10.1515\/9781400864041"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"P.-E. Moreau, C. Ringeissen, and M. Vittek. A pattern-matching compiler. In D. Parigot and M. van den Brand, editors, Proceedings of the 1st International Workshop on Language Descriptions, Tools and Applications, volume 44, Genova, april 2001. Electronic Notes in Theoretical Computer Science.","DOI":"10.1016\/S1571-0661(04)80926-5"},{"key":"15_CR15","series-title":"Lect Notes Comput Sci","first-page":"244","volume-title":"Procs. 5th international symposium on programming","author":"J.-P. Queille","year":"1981","unstructured":"J.-P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Procs. 5 th international symposium on programming, volume 137 of Lecture Notes in Computer Science, pages 244\u2013263. Springer Verlag, 1981."},{"key":"15_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/3-540-48685-2_11","volume-title":"Rewriting Techniques and Applications, 10th International Conference, RTA-99","author":"A. Rubio","year":"1999","unstructured":"A. Rubio. A Fully Syntactic AC-RPO. In P. Narendran and M. Rusinowitch, editors, Rewriting Techniques and Applications, 10th International Conference, RTA-99, LNCS 1631, pages 133\u2013147, Trento, Italy, July 2\u20134, 1999. Springer-Verlag."},{"key":"15_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1007\/3-540-53904-2_102","volume-title":"Rewriting Techniques and Applications, 4th International Conference, RTA-91","author":"R. Socher-Ambrosius","year":"1991","unstructured":"R. Socher-Ambrosius. Boolean Algebra Admits No Convergent Term Rewriting System. In R. V. Book, editor, Rewriting Techniques and Applications, 4th International Conference, RTA-91, LNCS 488, pages 264\u2013274, Como, Italy, Apr. 10\u201312, 1991. Springer-Verlag."},{"issue":"1","key":"15_CR18","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/FI-1998-33105","volume":"33","author":"L. Vigneron","year":"1998","unstructured":"L. Vigneron. Automated Deduction Techniques for Studying Rough Algebras. Fundamenta Informaticae, 33(1):85\u2013103, Feb. 1998.","journal-title":"Fundamenta Informaticae"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45610-4_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T20:25:51Z","timestamp":1587846351000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45610-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439165","9783540456100"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-45610-4_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}