{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:50:14Z","timestamp":1775868614601,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540600459","type":"print"},{"value":"9783540494133","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_40","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:37:05Z","timestamp":1330277825000},"page":"54-69","source":"Crossref","is-referenced-by-count":29,"title":["Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving"],"prefix":"10.1007","author":[{"given":"J\u00fcrgen","family":"Dingel","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Filkorn","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"issue":"2","key":"6_CR1","doi-asserted-by":"publisher","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, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"6_CR2","volume-title":"volume LNCS 131","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of programs: Workshop, Yorktown Heights, NY, May 1981, volume LNCS 131. Springer Verlag, 1981."},{"issue":"2","key":"6_CR3","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"1","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Programming Languages and Systems, 1(2):244\u2013263, 1986.","journal-title":"ACM Trans. Programming Languages and Systems"},{"key":"6_CR4","first-page":"343","volume-title":"Model checking and abstraction","author":"E.M. Clarke","year":"1992","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. In Proceedings of the 19th ACM Symposium on Principles of Programming Languages, pages 343\u2013354, New York, 1992. ACM Press."},{"key":"6_CR5","volume-title":"Technical Report ZFE BT SE 1-?","author":"J. Dingel","year":"1994","unstructured":"J. Dingel and T. Filkorn. Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving. Technical Report ZFE BT SE 1-?, Siemens AG, Corporate Research and Development, Munich, 1994. Draft."},{"key":"6_CR6","first-page":"344","volume-title":"Symbolic verification of sequential circuits synthesized with CALLAS","author":"T. Filkorn","year":"1992","unstructured":"T. Filkorn, M. Payer, and P. Warkentin. Symbolic verification of sequential circuits synthesized with CALLAS. In D. Gajski, editor, Proc. 6th International Workshop on High-Level Synthesis, pages 344\u2013353, Laguna Nigel, CA, U.S.A., November 1992. ACM\/IEEE."},{"key":"6_CR7","volume-title":"Technical Report ZFE BT SE 1-SVE-1","author":"T. Filkorn","year":"1994","unstructured":"Th. Filkorn, H.A. Schneider, A. Scholz, A. Strasser, and P. Warkentin. SVE User's Guide. Technical Report ZFE BT SE 1-SVE-1, Siemens AG, Corporate Research and Development, Munich, 1994."},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. In Computer Aided Verification, 5th International Conference, volume LNCS 697, pages 71\u201384. Springer Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_7"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"S. Graf. Verification of a distributed cache memory by using abstractions. In Computer Aided Verification, 6th International Conference, volume LNCS 818, pages 207\u2013219. Springer Verlag, 1994.","DOI":"10.1007\/3-540-58179-0_55"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Hardi Hungar. Combining model checking and theorem proving to verify parallel processes. In Computer Aided Verification, 5th International Conference, volume LNCS 697, pages 154\u2013165. Springer Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_13"},{"key":"6_CR11","unstructured":"David Long. Model Checking, Abstraction, and Compositional Verification. PhD thesis, Carnegie Mellon University, July 1993."},{"key":"6_CR12","unstructured":"Robin Milner. Communication and Concurrency. Prentise Hall, 1989."},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Elf: A meta-language for deductive systems. In Proceedings of CADE-12, volume LNAI 814, pages 811\u2013815. Springer Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_66"},{"key":"6_CR14","unstructured":"J. Quielle and J. Sifakis. Synthesis of synchronization skeletons for branching time temporal logic. In Proceedings of the 5th International Symposium in Programming, volume LNCS 137. Springer Verlag, 1981."},{"key":"6_CR15","volume-title":"A Guide to Seduct","year":"1994","unstructured":"Karl Stroetmann and Claus Bendix Nielsen, editors. A Guide to\nSeduct. Siemens AG, Munich, Germany, 1994."},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Pierre Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proceedings of Principles of Programming Languages 1986, pages 184\u2013193, 1986.","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_40.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:30:20Z","timestamp":1619573420000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}