{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:34Z","timestamp":1725663814517},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540578260"},{"type":"electronic","value":"9783540483465"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57826-9_137","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T08:26:38Z","timestamp":1330244798000},"page":"213-226","source":"Crossref","is-referenced-by-count":7,"title":["Alternative proof procedures for finite-state machines in higher-order logic"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Schneider","sequence":"first","affiliation":[]},{"given":"Ramayya","family":"Kumar","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Kropf","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"17_CR1","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In 5th Annual Symposium on Logic in Computer Science, 1990."},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, and D. E. Long. Representing circuits more efficiently in symbolic model checking. In 28th Design Automation Conference, pages 403\u2013407, 1991.","DOI":"10.1145\/127601.127702"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthet, and J.C. Madre. Verification of synchronous sequential machines based on symbolic execution. In Workshop on Automatic Verification Methods for Finite State Systems, pages 365\u2013373, Grenoble, June 1989.","DOI":"10.1007\/3-540-52148-8_30"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"J. Joyce and C. H. Seger. Linking BDD-Based Symbolic Evalutation to Interactive Theorem-Proving. In Proceedings of the 30 th Design Automation Conference, Dallas, Texas, 1993.","DOI":"10.1145\/157485.164981"},{"issue":"2","key":"17_CR5","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/BF01383880","volume":"2","author":"R. Kumar","year":"1993","unstructured":"R. Kumar, K. Schneider, and Th. Kropf. Structuring and automating hardware proofs in a higher-order theorem-proving environment. Journal of Formal Methods in System Design, 2(2):165\u2013223, 1993.","journal-title":"Journal of Formal Methods in System Design"},{"key":"17_CR6","first-page":"227","volume-title":"Higher Order Logic Theorem Proving and its Applications, volume A-20 of IFIP Transactions","author":"P. Loewenstein","year":"1992","unstructured":"P. Loewenstein. A formal theory of simulations between infinite automata. In L.J.M. Claesen and M. J.C. Gordon, editors, Higher Order Logic Theorem Proving and its Applications, volume A-20 of IFIP Transactions, pages 227\u2013246, Leuven, Belgium, 1992. North-Holland."},{"key":"17_CR7","first-page":"39","volume-title":"Higher Order Logic Theorem Proving and its Applications, volume A-20 of IFIP Transactions","author":"K. Schneider","year":"1992","unstructured":"K. Schneider, R. Kumar, and Th. Kropf. Efficient representation and computation of tableau proofs. In L.J.M. Claesen and M.J.C. Gordon, editors, Higher Order Logic Theorem Proving and its Applications, volume A-20 of IFIP Transactions, pages 39\u201358, Leuven, Belgium, 1992. North-Holland."},{"key":"17_CR8","unstructured":"K. Schneider, R. Kumar, and Th. Kropf. Hardware verification with first-order BDD's. In Conference on Computer Hardware Description Languages, 1993."},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"K. Schneider, R. Kumar, and Th. Kropf. Eliminating higher-order quanitifers to obtain decision procedures for hardware verification. In International Workshop on Higher-Order Logic Theorem Proving and its Applications, Vancouver, Canada, August 1993.","DOI":"10.1007\/3-540-57826-9_150"}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57826-9_137.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:14:27Z","timestamp":1605629667000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57826-9_137"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578260","9783540483465"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-57826-9_137","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}