{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:23:44Z","timestamp":1778297024641,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540631668","type":"print"},{"value":"9783540691952","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63166-6_53","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:14:46Z","timestamp":1330298086000},"page":"480-483","source":"Crossref","is-referenced-by-count":17,"title":["RuleBase: Model checking at IBM"],"prefix":"10.1007","author":[{"given":"I.","family":"Beer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Ben-David","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.","family":"Eisner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D.","family":"Geist","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L.","family":"Gluhovsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T.","family":"Heyman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Landver","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Paanah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Y.","family":"Rodeh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Ronin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Y.","family":"Wolfsthal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"53_CR1","unstructured":"I. Beer, S. Ben-David, C. Eisner, Y. Engel, R. Gewirtzman, and A. Landver, \u201cEstablishing PCI Compliance using Formal Verification: a Case Study\u201d, Intl. Phoenix Conf. on Comp. and Comm. 1995."},{"key":"53_CR2","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner and A. Landver, \u201cRuleBase: An Industry-Oriented Formal Verification Tool\u201d, Proceedings of the Design Automation Conference, DAC'96.","DOI":"10.1145\/240518.240642"},{"key":"53_CR3","unstructured":"I. Beer, S. Ben-David, C. Eisner and Y. Rodeh, \u201cEfficient Detection of Vacuity in ACTL Formulas\u201d, this issue."},{"key":"53_CR4","doi-asserted-by":"crossref","unstructured":"J. Burch, E. Clark and D. Long, \u201cRepresenting Circuits More Efficiently in Symbolic Model Checking\u201d, DAC'91, pp. 403\u2013407.","DOI":"10.1145\/127601.127702"},{"key":"53_CR5","first-page":"52","volume":"131","author":"E. Clarke","year":"1981","unstructured":"E. Clarke and E.A. Emerson, \u201cDesign and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic\u201d, in proc. Workshop on Logics of Programs, LNCS 131, pp. 52\u201371, 1981.","journal-title":"LNCS"},{"key":"53_CR6","doi-asserted-by":"crossref","unstructured":"A. Eiriksson and K. McMillan, \u201cUsing Formal Verification\/Analysis Methods on the Critical Path in System Design: A Case Study\u201d, CAV'95, LNCS 939, pp.367\u2013380.","DOI":"10.1007\/3-540-60045-0_63"},{"key":"53_CR7","unstructured":"C. Eisner, \u201cCC\/NUMA Formal Verification Project \u2014 Summary and Report\u201d, IBM Internal Memorandum, 1995."},{"key":"53_CR8","unstructured":"C. Eisner, \u201cAS\/400 SCU Formal Verification \u2014 Interim Report\u201d, IBM Internal Memorandum, 1997."},{"key":"53_CR9","unstructured":"C. Eisner, G. Shurek, G. Meil, R. Raghavan, \u201cCCP (Cache Coherence Protocol) Formal Verification Project Distributed Shared Memory Cache Coherence Protocol \u2014 Summary and Report\u201d, IBM Internal Memorandum, 1994."},{"key":"53_CR10","doi-asserted-by":"crossref","unstructured":"D. Geist and I. Beer, \u201cEfficient Model Checking by Automated Ordering of Transition Relation Partitions\u201d, CAV'94, LNCS 818, pp. 299\u2013310.","DOI":"10.1007\/3-540-58179-0_63"},{"key":"53_CR11","unstructured":"D. Long, \u201cModel Checking, Abstraction and Compositional Verification\u201d, Ph.D. Thesis, CMU, 1993."},{"key":"53_CR12","doi-asserted-by":"crossref","unstructured":"K. McMillan, \u201cSymbolic Model Checking\u201d, Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"53_CR13","doi-asserted-by":"crossref","unstructured":"K. Ravi and F. Somenzi, \u201cHigh-Density Reachability Analysis\u201d, Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD95), November 1995, San Jose, pp. 154\u2013158.","DOI":"10.1109\/ICCAD.1995.480006"},{"key":"53_CR14","unstructured":"R. Rudell, \u201cDynamic Variable Ordering for Ordered Binary Decision Diagrams\u201d, ICCAD'93, pp. 42\u201347."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63166-6_53.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:39:16Z","timestamp":1742600356000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63166-6_53"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631668","9783540691952"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-63166-6_53","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}