{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T14:58:24Z","timestamp":1770217104510,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540646082","type":"print"},{"value":"9783540693390","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028744","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"184-194","source":"Crossref","is-referenced-by-count":49,"title":["On-the-fly model checking of RCTL formulas"],"prefix":"10.1007","author":[{"given":"Ilan","family":"Beer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shoham","family":"Ben-David","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Avner","family":"Landver","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,18]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, A. Landver, \u201cRule-Base: an Industry-Oriented Formal Verification Tool\u201d, in Proc. 33rd Design Automation Conference 1996, pp. 655\u2013660.","DOI":"10.1145\/240518.240642"},{"key":"19_CR2","doi-asserted-by":"crossref","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, Berlin, 1981) pp. 52\u201371.","DOI":"10.1007\/BFb0025774"},{"key":"19_CR3","unstructured":"E.M. Clark and E.A. Emerson, \u201cCharacterizing Properties of Parallel Programs as Fixed-point\u201d, in Seventh International Colloquium on Automata, Languages, and Programming, Volume 85 of LNCS, 1981."},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"E. Clark, O. Grumberg and K. Hamaguchi, \u201cAnother Look at LTL Model Checking\u201d, Formal Methods in System Design, Volume 10, Number 1, Feb. 1997.","DOI":"10.1023\/A:1008615614281"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"B.Chen, M. Yamazaki, M. Fujita, \u201cBug Identification of a Real Chip Design by Symbolic Model Checking\u201d, Proc. European Design and Test Conference, 1994, pp. 132\u2013136.","DOI":"10.1109\/EDTC.1994.326886"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"A. Th. Eiriksson and K.L. McMillan, \u201cUsing Formal Verification\/ Analysis Methods on the Critical Path in System Design: A Case Study\u201d, 7th International Conference, CAV '95, pp. 367\u2013380.","DOI":"10.1007\/3-540-60045-0_63"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"O. Grumberg and D.E. Long, \u201cModel checking and modular verification\u201d, ACM Trans. on Programming Languages and Systems 16 (3), 1994.","DOI":"10.1145\/177492.177725"},{"key":"19_CR8","unstructured":"H. lwashita and T. Nakata, \u201cForward Model Checking Techniques Oriented to Buggy Designs\u201d, International Conference on Computer Aided Design, ICCAD '97."},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein an A. Pnueli, \u201cChecking that finite state concurrent programs satisfy their linear specification\u201d, Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, Jan. 1985.","DOI":"10.1145\/318593.318622"},{"key":"19_CR10","unstructured":"D. Long, \u201cModel Checking, Abstraction and Compositional Verification\u201d, Ph.D. Thesis, CMU, 1993."},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, \u201cSymbolic Model Checking\u201d, Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"19_CR12","unstructured":"Y Vardi and P Wolper \u201cAn automatic theoretic approach to automatic program verification\u201d, Proceeding of the First Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, June 1986."},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"P Wolper \u201cTemporal Logic can be more expressive\u201d, 22nd Annual Symposium on Foundation of Computer Science, Oct. 1981.","DOI":"10.1109\/SFCS.1981.44"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028744","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T08:23:38Z","timestamp":1586593418000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028744"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/bfb0028744","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]}}}