{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:39:53Z","timestamp":1725457193447},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540619376"},{"type":"electronic","value":"9783540495673"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0031809","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:59:01Z","timestamp":1134284341000},"page":"202-217","source":"Crossref","is-referenced-by-count":4,"title":["A unified approach for combining different formalisms for hardware verification"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Schneider","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Kropf","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"issue":"8","key":"14_CR1","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","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(8):677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"14_CR2","unstructured":"O. Coudert, C. Berthet, and J.C. Madre. Verification of sequential machines using boolean functional vectors. In L. Claesen, editor, IMEC-IFIP Workshop on Applied Formal Methods for Correct VLSI-Design, 1990."},{"issue":"2","key":"14_CR3","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, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. Information and Computing, 98(2):142\u2013170, June 1992.","journal-title":"Information and Computing"},{"key":"14_CR4","unstructured":"M.J.C. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G.J. Milne and P.A. Subrahmanyam, editors, Formal Aspects of VLSI Design, pages 153\u2013177. Computer Laboratory, University of Cambridge, 1986."},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"R. Kumar, K. Schneider, and T. Kropf. Structuring and Automating Hardware Proofs in a Higher-Order Theorem-Proving Environment. International Journal of Formal System Design, pages 165\u2013230, 1993.","DOI":"10.1007\/BF01383880"},{"key":"14_CR6","first-page":"258","volume-title":"volume 901 of Lecture Notes in Computer Science","author":"S. Owre","year":"1994","unstructured":"S. Owre, J.M. Rushby, N. Shankar, and M.K. Srivas. A tutorial on using PVS for hardware verification. In T. Kropf and R. Kumar, editors, Proc. 2nd International Conference on Theorem Provers in Circuit Design (TPCD94), volume 901 of Lecture Notes in Computer Science, pages 258\u2013279, Bad Herrenalb, Germany, September 1994. Springer-Verlag, published 1995."},{"key":"14_CR7","first-page":"353","volume-title":"Compositional Model Checking","author":"E.M. Clarke","year":"1989","unstructured":"E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional Model Checking. In Proceedings of Fourth Annual Symposium on Logic in Computer Science, pages 353\u2013361, Washington D.C., June 1989. IEEE Computer Society Press."},{"key":"14_CR8","volume-title":"Model Checking and Abstraction","author":"E. Clarke","year":"1992","unstructured":"E. Clarke, O. Grumberg, and D. Long. Model Checking and Abstraction. In Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages, New York, January 1992. ACM."},{"key":"14_CR9","unstructured":"D.E. Long. Model Checking, Abstraction, and Compositional Verification. PhD thesis, Carnegie Mellon University, 1993."},{"key":"14_CR10","first-page":"648","volume-title":"Control-Path Oriented Verification of Sequential Generic Circuits with Control and Data Path","author":"K. Schneider","year":"1994","unstructured":"K. Schneider, T. Kropf, and R. Kumar. Control-Path Oriented Verification of Sequential Generic Circuits with Control and Data Path. In Proceeding of the European Design and Test Conference, pages 648\u2013652, Paris, France, March 1994. IEEE Computer Society Press."},{"key":"14_CR11","first-page":"208","volume-title":"EDAC94","author":"M. Langevin","year":"1994","unstructured":"M. Langevin, E. Cerny, and R.E. Ladner. An extended OBDD representation for extended FSMs. In The European Design and Test Conference, pages 208\u2013303, Paris, February 1994. IEEE Computer Society Press. EDAC94."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"R. Hojati and R.K. Brayton. Automatic Datapath Abstraction in Hardware Systems. In Proc. of the International Conference on Computer-Aided Verification, pages 98\u2013113. Springer Verlag, LNCS, 1995.","DOI":"10.1007\/3-540-60045-0_43"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"H. Hungar, O. Grumberg, and W. Damm. What if model checking must be truly symbolic. In P.E. Camurati and H. Eveking, editors, Correct Hardware Design and Verification Methods, volume 987 of Lecture Notes in Computer Science, pages 1\u201320, October 1995. IFIP WG10.5 Advanced Research Working Conference CHARME'95, Springer-Verlag.","DOI":"10.1007\/3-540-60385-9_1"},{"key":"14_CR14","volume-title":"Technical Report CMU-CS-95-161","author":"E. Clarke","year":"1995","unstructured":"E. Clarke and X. Zhao. Word level symbolic model checking. Technical Report CMU-CS-95-161, Carnegie Mellon University, Pittsburgh, PA 15213, May 1995."},{"key":"14_CR15","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"14_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993."},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"D. Kapur and H. Zhang. RRL: a rewrite rule laboratory. In Lusk and Overbeek, editors, 9th International Conference on Automated Deduction, pages 768\u2013769. Springer-Verlag, 1988.","DOI":"10.1007\/BFb0012889"},{"key":"14_CR18","isbn-type":"print","volume-title":"volume 116 of DISKI (Dissertationen zur K\u00fcnstlichen Intelligenz)","author":"K. Schneider","year":"1996","unstructured":"K. Schneider. Ein einheitlicher Ansatz zur Unterst\u00fctzung von Abstraktionsmechanismen der Hardwareverifikation, volume 116 of DISKI (Dissertationen zur K\u00fcnstlichen Intelligenz). Infix Verlag, Sankt Augustin, 1996. ISBN 3-89601-116-2.","ISBN":"http:\/\/id.crossref.org\/isbn\/3896011162"},{"key":"14_CR19","first-page":"129","volume-title":"VLSI Specification, Verification, and Synthesis","author":"T.F. Melham","year":"1988","unstructured":"T.F. Melham. Abstraction mechanisms for hardware verification. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis, pages 129\u2013157, Boston, 1988. Kluwer Academic Publishers."},{"key":"14_CR20","first-page":"996","volume-title":"Handbook of Theoretical Computer Science, volume B","author":"E.A. Emerson","year":"1990","unstructured":"E.A. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 996\u20131072, Amsterdam, 1990. Elsevier Science Publishers."},{"key":"14_CR21","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","volume":"25","author":"G. Huet","year":"1982","unstructured":"G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, 25:239\u2013266, 1982.","journal-title":"Journal of Computer and System Sciences"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"L. Fribourg. A strong restriction of the inductive completion procedure. In 13th International Colloqium on Automata, Languages and Programming, pages 105\u2013115, 1986.","DOI":"10.1007\/3-540-16761-7_60"},{"key":"14_CR23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(89)90062-X","volume":"82","author":"J.-P. Jouannaud","year":"1989","unstructured":"J.-P. Jouannaud and E. Kounalis. Proofs by induction in equational theories without constructors. Information and Computation, 82:1\u201333, 1989.","journal-title":"Information and Computation"},{"key":"14_CR24","first-page":"379","volume":"10","author":"L. Staiger","year":"1974","unstructured":"L. Staiger and K.W. Wagner. Automatentheoretische Charakterisierungen topologischer Klassen regul\u00e4rer Folgenmengen. Elektron. Informationsverarb. Kybernet., 10:379\u2013392, 1974.","journal-title":"Elektron. Informationsverarb. Kybernet."},{"key":"14_CR25","unstructured":"K. Schneider. Translating LTL Model Checking to CTL Model Checking. Technical Report SFB358-C2-3\/96, Universit\u00e4t Karlsruhe, Institut f\u00fcr Rechnerentwurf und Fehlertoleranz, January 1996."},{"key":"14_CR26","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12:576\u2013580, 1969.","journal-title":"Communications of the ACM"},{"key":"14_CR27","unstructured":"M. Machtey and P.Young. An Introduction to the General Theory of Algorithms. North-Holland, 1978."},{"key":"14_CR28","unstructured":"R.S. Boyer and J.S. Moore. A Computational Logic Handbook. Academic Press, 1979."},{"key":"14_CR29","first-page":"177","volume-title":"volume 859 of Lecture Notes in Computer Science","author":"P. Curzon","year":"1994","unstructured":"P. Curzon. Tracking design changes with formal verification. In T.F. Melham and J. Camilleri, editors, International Workshop on Higher Order Logic Theorem Proving and its Applications, volume 859 of Lecture Notes in Computer Science, pages 177\u2013192, Malta, September 1994. Springer-Verlag."},{"key":"14_CR30","first-page":"46","volume-title":"Sequential Circuit Verification Using Symbolic Model Checking","author":"J.R. Burch","year":"1990","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill. Sequential Circuit Verification Using Symbolic Model Checking. In Proceedings of the 27th ACM\/IEEE Design Automation Conference, pages 46\u201351, Los Alamitos, CA, June 1990 ACM\/IEEE, IEEE Society Press."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0031809","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T13:49:32Z","timestamp":1586612972000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0031809"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540619376","9783540495673"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/bfb0031809","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}