{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T12:39:52Z","timestamp":1760099992714},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662020"},{"type":"electronic","value":"9783540486831"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"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":[[1999]]},"DOI":"10.1007\/3-540-48683-6_32","type":"book-chapter","created":{"date-parts":[[2007,10,7]],"date-time":"2007-10-07T03:22:18Z","timestamp":1191727338000},"page":"369-379","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation"],"prefix":"10.1007","author":[{"given":"Panagiotis","family":"Manolios","sequence":"first","affiliation":[]},{"given":"Kedar","family":"Namjoshi","sequence":"additional","affiliation":[]},{"given":"Robert","family":"Sumners","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,1,14]]},"reference":[{"key":"32_CR1","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model checking for real time systems. In 5th IEEE Symp. on Logic in Computer Science, 1990."},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2), 1996.","DOI":"10.1006\/inco.1996.0053"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"M. Browne, E.M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59, 1988.","DOI":"10.21236\/ADA188620"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"M.A. Bezem and J.F. Groote. A correctness proof of a one bit sliding window protocol in mCRL. The Computer Journal, 1994.","DOI":"10.1093\/comjnl\/37.7.651"},{"key":"32_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Conference on Computer Aided Verification","author":"B. Boigelot","year":"1996","unstructured":"B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDD\u2019s. In Conference on Computer Aided Verification, volume 1102 of LNCS, 1996."},{"key":"32_CR6","unstructured":"R. Boyer and J. Moore. A Computational Logic. Kluwer Academic Publishers, 1979."},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"K.A. Barlett, R.A. Scantlebury, and P.C. Wilkinson. A note on reliable full duplex transmission over half duplex links. In Communications of the ACM, volume 12, 1969.","DOI":"10.1145\/362946.362970"},{"key":"32_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Workshop on Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop on Logics of Programs, volume 131 of LNCS. Springer-Verlag, 1981."},{"key":"32_CR9","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic. ACM Transactions on Programming Languages and Systems, 8(2), 1986.","DOI":"10.1145\/5397.5399"},{"issue":"1","key":"32_CR10","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E. A. Emerson","year":"1986","unstructured":"E. A. Emerson and J. Y. Halpern. \u201cSometimes\u201d and \u201cnot never\u201d revisited: on branching versus linear time temporal logic. JACM, 33(1):151\u2013178, January 1986.","journal-title":"JACM"},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and K.S. Namjoshi. Reasoning about rings. In ACM Symposium on Principles of Programming Languages, 1995.","DOI":"10.1145\/199448.199468"},{"key":"32_CR12","unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"32_CR13","doi-asserted-by":"crossref","unstructured":"S. German and A.P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 1992.","DOI":"10.1145\/146637.146681"},{"key":"32_CR14","series-title":"Lect Notes Comput Sci","volume-title":"Conference on Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In Conference on Computer Aided Verification, volume 1254 of LNCS, 1997."},{"key":"32_CR15","series-title":"Lect Notes Comput Sci","volume-title":"Formal Methods Europe (FME)","author":"K. Havelund","year":"1996","unstructured":"K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe (FME), volume 1051 of LNCS. Springer-Verlag, 1996."},{"issue":"4","key":"32_CR16","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M. Kaufmann","year":"1997","unstructured":"M. Kaufmann and J S. Moore. An industrial strength theorem prover for a logic based on Common Lisp. IEEE Transactions on Software Engineering, 23(4):203\u2013213, April 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"L. Lamport. \u201cSometimes\u201d is sometimes \u201cnot never\u201d. In ACM Symposium on Principles of Programming Languages, 1980.","DOI":"10.1145\/567446.567463"},{"key":"32_CR18","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall, 1990."},{"key":"32_CR19","doi-asserted-by":"crossref","unstructured":"O. M\u00fcller and T. Nipkow. Combining model checking and deduction for I\/O-Automata. In Proceedings of TACAS, 1995.","DOI":"10.1007\/3-540-60630-0_1"},{"key":"32_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/BFb0058037","volume-title":"17th Conference on Foundations of Software Technology and Theoretical Computer Science","author":"K. S. Namjoshi","year":"1997","unstructured":"K. S. Namjoshi. A simple characterization of stuttering bisimulation. In 17th Conference on Foundations of Software Technology and Theoretical Computer Science, volume 1346 of LNCS, pages 284\u2013296, 1997."},{"key":"32_CR21","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the 5th International Symposium on Programming","author":"J.P. Queille","year":"1982","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. of the 5th International Symposium on Programming, volume 137 of LNCS, 1982."},{"key":"32_CR22","doi-asserted-by":"crossref","unstructured":"P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages, pages 184\u2013193. ACM Press, 1986.","DOI":"10.1145\/512644.512661"}],"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-48683-6_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T06:07:56Z","timestamp":1586153276000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48683-6_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662020","9783540486831"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-48683-6_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"14 January 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}