{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T23:07:23Z","timestamp":1768259243079,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540631668","type":"print"},{"value":"9783540691952","type":"electronic"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63166-6_41","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:14:05Z","timestamp":1330280045000},"page":"424-435","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":39,"title":["Symbolic model checking with rich assertional languages"],"prefix":"10.1007","author":[{"given":"Y.","family":"Resten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"O.","family":"Maler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Marcus","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"E.","family":"Shahar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"41_CR1","doi-asserted-by":"crossref","unstructured":"K. R. Apt and D. Kozen. Limits for automatic program verification of finite-state concurrent systems. Information Processing Letters, 22(6), 1986.","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"41_CR2","doi-asserted-by":"crossref","unstructured":"N. Bj\u00f8rner, I.A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. In LNCS 976, 1995.","DOI":"10.1007\/3-540-60299-2_37"},{"key":"41_CR3","doi-asserted-by":"crossref","unstructured":"R.V. Book and F. Otto. String-Rewriting Systems, Springer, 1993.","DOI":"10.1007\/978-1-4613-9771-7"},{"key":"41_CR4","unstructured":"A. Bouajjani and O. Maler, Reachability Analysis of Push-down Automata. Workshop on Infinite-state Systems, Pisa, 1996."},{"key":"41_CR5","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg. Reasoning about networks with many finite state processes. In PODC'86."},{"issue":"2","key":"41_CR6","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, et al. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"41_CR7","doi-asserted-by":"crossref","unstructured":"D.A. Basin and N. Klarlund. Hardware verification using 2nd-order logic. In P. Wolper, editor, CAV'95, LNCS 939, 1995.","DOI":"10.7146\/brics.v2i7.19509"},{"key":"41_CR8","doi-asserted-by":"crossref","unstructured":"S. Bensalem, Y. Lakhnech, and H. Saidi. Powerful techniques for the automatic generation of invariants. CAV'96, 1996.","DOI":"10.1007\/3-540-61474-5_80"},{"issue":"12","key":"41_CR9","doi-asserted-by":"crossref","first-page":"1035","DOI":"10.1109\/TC.1986.1676711","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(12):1035\u20131044, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"41_CR10","unstructured":"E.M. Clarke and E.A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. Logics of Programs, LNCS 131, 1981."},{"key":"41_CR11","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, et al. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Trans. Prog. Lang. Sys., 1986.","DOI":"10.1145\/5397.5399"},{"key":"41_CR12","unstructured":"E.M. Clarke, O. Grumberg, et al. Verification of the futurebus+ cache coherence protocol. Proceedings of the Eleventh International Symposium on Computer Hardware Description Languages and their Applications. 1993."},{"key":"41_CR13","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and S. Jha. Verifying parameterized networks using abstraction and regular languages. In CONCUR'95, 1995.","DOI":"10.1007\/3-540-60218-6_30"},{"key":"41_CR14","doi-asserted-by":"crossref","unstructured":"J. Doner. Tree Acceptors and some of their applications, JCSS 4, 1970.","DOI":"10.1016\/S0022-0000(70)80041-1"},{"key":"41_CR15","doi-asserted-by":"crossref","unstructured":"E. A. Emerson, K. S. Namjoshi. Reasoning about rings. POPL'95, 1995.","DOI":"10.1145\/199448.199468"},{"key":"41_CR16","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and K.S. Namjoshi. Automatic verification of parameterized synchronous systems. In R. Alur and T. Henzinger, editors, CAV'96, 1996.","DOI":"10.1007\/3-540-61474-5_60"},{"key":"41_CR17","unstructured":"F. Gecseg and M. Steinby. Tree Automata Akademiai Kiado, 1984."},{"key":"41_CR18","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, F. Lagnier, et al. An experience in proving regular networks of processes by modular model checking. Acta Informatica, 29(6\/7), 1992.","DOI":"10.1007\/BF01185559"},{"key":"41_CR19","unstructured":"J.G. Henriksen, J. Jensen, et al. Mona: Monadic second-order logic in practice. In TACAS '95, LNCS 1019, 1996."},{"key":"41_CR20","unstructured":"C.N. Ip and D. Dill. Verifying systems with replicated components in Mun\u03d5. In R. Alur and T. Henzinger, editors, CAV'96, 1996."},{"key":"41_CR21","doi-asserted-by":"crossref","unstructured":"O. Kupferman and O. Grumberg. Branching Time Temporal Logic and Amorphous Tree Automata. Information and Computation 125, 1996.","DOI":"10.1006\/inco.1996.0021"},{"key":"41_CR22","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan and K. McMillan. A structural induction theorem for processes. In P. Rudnicki, editor, PODC'89, Edmonton, AB, Canada, 1989.","DOI":"10.1145\/72981.72998"},{"key":"41_CR23","doi-asserted-by":"crossref","unstructured":"D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In POPL'97, Paris, 1997.","DOI":"10.1145\/263699.263747"},{"key":"41_CR24","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Anuchitanukul, et al. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Stanford University, 1994.","DOI":"10.21236\/ADA324036"},{"key":"41_CR25","doi-asserted-by":"crossref","unstructured":"K.L McMillan. Symbolic Model Checking. 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"41_CR26","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995."},{"key":"41_CR27","doi-asserted-by":"crossref","unstructured":"A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic verification. In R. Alur and T. Henzinger, editors, CAV'96, 1996.","DOI":"10.1007\/3-540-61474-5_68"},{"key":"41_CR28","doi-asserted-by":"crossref","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in cesar. International Symposium on Programming,LNCS 137, 1982.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"41_CR29","doi-asserted-by":"crossref","unstructured":"Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. In LNCS 407, 1989.","DOI":"10.1007\/3-540-52148-8_13"},{"key":"41_CR30","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"A.P. Sistla","year":"1992","unstructured":"A.P. Sistla and S.M. German. Reasoning about systems with many processes. J. ACM, 39:675\u2013735, 1992.","journal-title":"J. ACM"},{"key":"41_CR31","volume-title":"Technical report","author":"N. Shankar","year":"1993","unstructured":"N. Shankar, S. Owre, and J.M. Rushby. The PVS proof checker: A reference manual (draft). Technical report, SRI International, Menlo Park, CA, 1993."},{"key":"41_CR32","doi-asserted-by":"crossref","unstructured":"J.W. Thatcher, J.B. Wright. Generalized finite automata with application to a decision procedure in second order logic. Math. Sys. Theory 2, 1968.","DOI":"10.1007\/BF01691346"},{"key":"41_CR33","doi-asserted-by":"crossref","unstructured":"P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In LNCS 407, 1989.","DOI":"10.1007\/3-540-52148-8_6"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63166-6_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:36:56Z","timestamp":1558255016000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63166-6_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631668","9783540691952"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-63166-6_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"7 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}