{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:50:52Z","timestamp":1725490252882},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665878"},{"type":"electronic","value":"9783540481195"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48119-2_17","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T21:23:00Z","timestamp":1188336180000},"page":"272-288","source":"Crossref","is-referenced-by-count":3,"title":["Symbolic Model Checking with Fewer Fixpoint Computations"],"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"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"R. J. Anderson, P. Beame, S. Burns, W. Chan, F. Modugno, D. Notkin, and R. Reese. Model checking large software specifications. In 4th Symposium on the Foundations of Software Engineering, pages 156\u2013166. ACM\/SIGSOFT, Oct. 1996.","DOI":"10.1145\/239098.239127"},{"key":"17_CR2","series-title":"Lect Notes Comput Sci","volume-title":"TACAS\u201999","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without bdds. In TACAS\u201999, Lecture Notes in Computer Science. Springer Verlag."},{"issue":"35","key":"17_CR3","first-page":"1035","volume":"C","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant. Graphbased algorithm for boolean function manipulation. IEEE Transactions Computers, C(35):1035\u20131044, 1986.","journal-title":"IEEE Transactions Computers"},{"key":"17_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.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons for branching time temporal logic. In Logics of Programs: Workshop, volume 131 of Lecture Notes in Computer Science, pages 52\u201371. Springer Verlag, 1981."},{"issue":"2","key":"17_CR5","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions On Programming Languages and Systems, 8(2):244\u2013263, Apr. 1986.","journal-title":"ACM Transactions On Programming Languages and Systems"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. In 19th Annual ACM Symposium on Principles of Programming Languages, 1992.","DOI":"10.1145\/143165.143235"},{"key":"17_CR7","unstructured":"E.M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D.E. Long, K.L. McMillan, and L.A. Ness. Verification of the futurebus+cache coherence protocol. In L. Claesen, editor, 11th International Symposium on Computer Hardware Description Languages: CHDL\u201993. NorthHolland, 1993."},{"key":"17_CR8","unstructured":"E.M. Clarke, T. Filkorn, and S. Jha. Exploiting symmetry in temporal logic model checking."},{"key":"17_CR9","unstructured":"D. D\u00e9harbe. V\u00e9rification Symbolique de Mod\u00e8le pour la logique CTL: \u00c9tude et Application au Langage VHDL. PhD thesis, Universit\u00e9 Joseph Fourier-Grenoble 1, Nov. 1996."},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"D. D\u00e9harbe and A. Martins Moreira. Using induction and BDDs to model check invariants. In Hon F. Li and David K. Probst, editors, CHARME\u201997: Correct Hardware Design and Verification Methods, Montr\u00e9al, Canada, Oct. 1997. Chapman & Hall.","DOI":"10.1007\/978-0-387-35190-2_13"},{"key":"17_CR11","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"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Bernhard Josko. MCTL-an extension of CTL for modular verification of concurrent systems. pages 165\u2013187, 1987.","DOI":"10.1007\/3-540-51803-7_25"},{"key":"17_CR13","series-title":"PhD thesis","volume-title":"PRIAM Un outil de v\u00e9rification formelle des circuits int\u00e9gr\u00e9s digitaux","author":"J.C. Madre","year":"1990","unstructured":"J.C. Madre. PRIAM Un outil de v\u00e9rification formelle des circuits int\u00e9gr\u00e9s digitaux. PhD thesis, Ecole nationale sup\u00e9rieure des t\u00e9l\u00e9communications, Paris, France, June 1990. 90 E 007."},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"17_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":"17_CR16","unstructured":"B. Yang. Fmcad\u201998 benchmark traces. http:\/\/www.cs.cmu.edu\/~bwolen\/fmcad98 ."}],"container-title":["Lecture Notes in Computer Science","FM\u201999 \u2014 Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48119-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T13:27:26Z","timestamp":1556803646000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48119-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665878","9783540481195"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-48119-2_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}