{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:20:32Z","timestamp":1725488432086},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425250"},{"type":"electronic","value":"9783540447559"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44755-5_17","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T06:03:32Z","timestamp":1186725812000},"page":"233-248","source":"Crossref","is-referenced-by-count":5,"title":["Representing Hierarchical Automata in Interactive Theorem Provers"],"prefix":"10.1007","author":[{"given":"Steffen","family":"Helke","sequence":"first","affiliation":[]},{"given":"Florian","family":"Kamm\u00fcller","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"J. Burghardt, F. Kamm\u00fcller, J. Sanders. On the Antisymmetry of Galois Embeddings. Information Processing Letters, 79:2, Elsevier, June 2001.","DOI":"10.1016\/S0020-0190(00)00176-9"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract Interpretation. In Principles of Programming Languages, ACM Press, 1977.","DOI":"10.1145\/512950.512973"},{"key":"17_CR3","volume-title":"Model Checking","author":"E. M. Clarke","year":"1999","unstructured":"Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999."},{"key":"17_CR4","series-title":"Lect Notes Comput Sci","first-page":"338","volume-title":"International Meeting on Higher-Order Logic Theorem Proving and its Applications","author":"N. Day","year":"1993","unstructured":"Nancy Day and Jeffrey Joyce. The Semantics of Statecharts in HOL. In International Meeting on Higher-Order Logic Theorem Proving and its Applications. Springer LNCS, 780:338\u2013351, 1993."},{"issue":"4","key":"17_CR5","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D. Harel","year":"1996","unstructured":"D. Harel and D. Naamad. A STATEMATE semantics for statecharts. ACM Trans. on Software Engineering and Methodology, 5(4):293\u2013333, Oct 1996.","journal-title":"ACM Trans. on Software Engineering and Methodology"},{"key":"17_CR6","unstructured":"F. Kamm\u00fcller and S. Helke. Mechanical Analysis of UML State Machines and Class Diagrams. In Defining Precise Semantics for UML, Sophia Antipolis, France, June 2000. Satellite Workshop, ECOOP 2000."},{"key":"17_CR7","series-title":"PhD thesis","volume-title":"Semantics and Verification of Statecharts","author":"E. Mikk","year":"2000","unstructured":"E. Mikk. Semantics and Verification of Statecharts. PhD thesis, Christian-Albrechts-Universit\u00e4t, Kiel. Bericht Nr. 2001, October 2000."},{"key":"17_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-60580-0","volume-title":"TACAS\u201995, Tools and Algorithms for the Construction and Analysis of Systems","author":"O. M\u00fcller","year":"1995","unstructured":"Olaf M\u00fcller and Tobias Nipkow. Combining Model Checking and Deduction for I\/O Automata. In TACAS\u201995, Tools and Algorithms for the Construction and Analysis of Systems, Springer LNCS, 1019:1\u201316, 1995."},{"key":"17_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1007\/3-540-60579-7_6","volume-title":"Types for Proofs and Programs","author":"T. Nipkow","year":"1995","unstructured":"T. Nipkow and K. Slind. I\/O Automata in Isabelle\/HOL. In Types for Proofs and Programs, Springer LNCS, 996:101\u2013119, 1995."},{"key":"17_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, Springer LNCS, 828, 1994."},{"key":"17_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_38","volume-title":"11th International Conference on Computer Aided Verification, CAV\u201999","author":"H. Sa\u00efdi","year":"1999","unstructured":"Hassen Sa\u00efdi and Natarajan Shankar. Abstract and Model Check While You Prove. In N. Halbwachs and D. Peled, editors, 11th International Conference on Computer Aided Verification, CAV\u201999, Springer LNCS, 1633, 1999."},{"key":"17_CR12","series-title":"Lect Notes Comput Sci","first-page":"128","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"M. Beeck von der","year":"1994","unstructured":"M. von der Beeck. A Comparison of Statechart Variants\/ In Formal Techniques in Real-Time and Fault-Tolerant Systems. Springer LNCS, 863: 128\u2013148, 1994."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44755-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T18:10:49Z","timestamp":1556734249000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44755-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425250","9783540447559"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-44755-5_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}