{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:30:14Z","timestamp":1755217814701,"version":"3.43.0"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2001,7,1]],"date-time":"2001-07-01T00:00:00Z","timestamp":993945600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,7,1]],"date-time":"2001-07-01T00:00:00Z","timestamp":993945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2001,7]]},"DOI":"10.1023\/a:1011219209077","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T04:18:21Z","timestamp":1040617101000},"page":"35-44","source":"Crossref","is-referenced-by-count":5,"title":["On the Effective Deployment of Functional Formal Verification"],"prefix":"10.1007","volume":"19","author":[{"given":"Yael","family":"Abarbanel-Vinov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neta","family":"Aizenbud-Reshef","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ilan","family":"Beer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cindy","family":"Eisner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Geist","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tamir","family":"Heyman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Iris","family":"Reuveni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eran","family":"Rippel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Irit","family":"Shitsevalov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yaron","family":"Wolfsthal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tali","family":"Yatzkar-Haham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"325207_CR1","doi-asserted-by":"crossref","unstructured":"J. Baumgartner and T. Heyman, \u201cAn overview and application of model reduction techniques in formal verification,\u201d in Proc. IEEE IPCCC, Phoenix, Arizona, pp. 165\u2013171, 1998.","DOI":"10.1109\/PCCC.1998.659939"},{"key":"325207_CR2","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, and A. Landver, \u201cRuleBase: An industry-oriented formal verification tool,\u201d in Proc. 33rd Design Automation Conference, 1996, Las Vegas, Nevada, pp. 655\u2013660.","DOI":"10.1109\/DAC.1996.545656"},{"key":"325207_CR3","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh, \u201cEfficient detection of vacuity in ACTL formulas,\u201d in Proc. CAV '97, Springer-Verlag, Haifa, Israel, pp. 279\u2013290.","DOI":"10.1007\/3-540-63166-6_28"},{"key":"325207_CR4","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, and A. Landver, \u201cOn-the-fly model checking of RCTL formulas,\u201d in Proc. CAV '98, Springer-Verlag, Vancouver, BC, Canada, pp. 184\u2013194.","DOI":"10.1007\/BFb0028744"},{"key":"325207_CR5","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","volume":"131","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson, \u201cDesign and synthesis of synchronization skeletons using branching time temporal logic,\u201d in Proc. Workshop on Logics of Programs, Lecture Notes in Computer Science, Vol. 131, Springer-Verlag, Berlin, 1981, pp. 52\u201371.","journal-title":"Proc. Workshop on Logics of Programs"},{"key":"325207_CR6","doi-asserted-by":"crossref","unstructured":"C. Eisner, R. Hoover, W. Nation, K. Nelson, I. Shitsevalov, and K. Valk, \u201cA methodology for formal design of hardware control with application to cache coherence protocols,\u201d in Proc. DAC 2000, Los Angeles, California, pp. 724\u2013729.","DOI":"10.1145\/337292.337757"},{"key":"325207_CR7","doi-asserted-by":"crossref","unstructured":"D. Geist and I. Beer, \u201cEfficient model checking by automated ordering of transition relation partitions,\u201d in CAV 1994, LNCS 818, Stanford, California, pp. 299\u2013310.","DOI":"10.1007\/3-540-58179-0_63"},{"key":"325207_CR8","unstructured":"G. Lippert and D. Freerksen, \u201cNorthstar SCU formal verification,\u201d Internal Memo, 1997."},{"key":"325207_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"K.L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Boston\/Dordrecht\/London, 1993."},{"key":"325207_CR10","unstructured":"PCI specifications, www.pcisig.com\/tech\/index.html"},{"key":"325207_CR11","unstructured":"PowerPC User Manuals, www.chips.ibm.com\/techlib\/products\/powerpc\/manuals"},{"key":"325207_CR12","doi-asserted-by":"crossref","unstructured":"K. Ravi and F. Somenzi, \u201cHigh-density reachability analysis,\u201d in Proc. Intl. Conference on Computer-Aided Design (ICCAD '95), San Jose, California, pp. 154\u2013158.","DOI":"10.1109\/ICCAD.1995.480006"},{"key":"325207_CR13","doi-asserted-by":"crossref","unstructured":"A.L. Sangiovanni-Vincentelli, P.C. McGeer, and A. Saldanha, \u201cVerification of electronic systems,\u201d in Proc. DAC '96, Las Vegas, Nevada, pp. 106\u2013111.","DOI":"10.1145\/240518.240539"},{"key":"325207_CR14","unstructured":"www.chips.ibm.com\/products\/asics\/cores\/briefs\/agp 2x.html"},{"key":"325207_CR15","unstructured":"www.llnl.gov\/sccd\/lc\/asci"},{"key":"325207_CR16","doi-asserted-by":"crossref","unstructured":"C.H. Yang and D.L. Dill, \u201cValidation with guided search of the state space,\u201d in Proc. DAC '98, San Francisco, California, pp. 599\u2013604.","DOI":"10.1145\/277044.277201"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011219209077.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1011219209077\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011219209077.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T20:13:53Z","timestamp":1754424833000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1011219209077"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,7]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2001,7]]}},"alternative-id":["325207"],"URL":"https:\/\/doi.org\/10.1023\/a:1011219209077","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2001,7]]}}}