{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T21:10:18Z","timestamp":1737321018043,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664628"},{"type":"electronic","value":"9783540482574"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48257-1_5","type":"book-chapter","created":{"date-parts":[[2007,7,20]],"date-time":"2007-07-20T20:25:09Z","timestamp":1184963109000},"page":"92-106","source":"Crossref","is-referenced-by-count":0,"title":["Structured Formal Verification of a Fragment of the IBM S\/390 Clock Chip"],"prefix":"10.1007","author":[{"given":"Alfons","family":"Geser","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"K\u00fcchlin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"12","key":"5_CR1","doi-asserted-by":"crossref","first-page":"1035","DOI":"10.1109\/TC.1986.1676711","volume":"35","author":"M. C. Browne","year":"1986","unstructured":"M. C. Browne, E. M. Clarke, D. L. Dill, and B. Mishra. Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computers, 35(12):1035\u20131045, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"5_CR2","unstructured":"J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic Model Checking for Sequential Circuit Verification. Technical Report CMU-CS-93-211, Carnegie Mellon University, July 1993."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Reinhard B\u00fcndgen and Wolfgang K\u00fcchlin. Term rewriting as a tool for hardware and software codesign. In Jerzy Rosenblit and Klaus Buchenrieder, editors, Codesign \u2014 Computer-Aided Software\/Hardware Engineering, pages 19\u201340. IEEE Press, 1995.","DOI":"10.1049\/ic:19951042"},{"key":"5_CR4","unstructured":"Reinhard B\u00fcndgen and Wolfgang K\u00fcchlin. Verification of the Sparrow processor. In Proc. Engineering of Computer-Based Systems (ECBS). IEEE Press, 1996."},{"key":"5_CR5","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1090\/conm\/029\/07","volume":"29","author":"R. S. Boyer","year":"1984","unstructured":"Robert S. Boyer and J. Strother Moore. Proof-checking, theorem-proving, and program verification. Contemporary Mathematics, 29:119\u2013132, 1984.","journal-title":"Contemporary Mathematics"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"R.E. Bryant. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams. ACM Comp. Surveys, 24(3), Sept. 1992.","DOI":"10.1145\/136035.136043"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Bruno Courcelle. Graph rewriting: An algebraic and logic approach. In van Leeuwen [vL94], chapter 5, pages 193\u2013242.","DOI":"10.1016\/B978-0-444-88074-1.50010-X"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Mandalagiri S. Chandrasekhar, John P. Privitera, and Kenneth W. Conradt. Application of term rewriting techniques to hardware design verification. In 24thACM\/IEEE Design Automation Conference (DAC), pages 277\u2013283, 1987.","DOI":"10.1145\/37888.37930"},{"issue":"1&2","key":"5_CR9","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Nachum Dershowitz. Termination of rewriting. J. Symb. Comput., 3(1&2):69\u2013115, Feb.\/April 1987. Corrigendum: 4, 3, Dec. 1987, 409\u2013410.","journal-title":"J. Symb. Comput."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In van Leeuwen [vL94], chapter 6, pages 243\u2013320.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"5_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BFb0015045","volume-title":"Algebraic methods: Theory, Tools, and Applications","author":"A. Geser","year":"1987","unstructured":"Alfons Geser. A specification of the intel 8085 microprocessor \u2014 a case study. In Martin Wirsing and Jan A. Bergstra, editors, Algebraic methods: Theory, Tools, and Applications, LNCS 394, pages 347\u2013402. Springer, June 1987."},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"A. Gupta. Formal Hardware Verification: A Survey. Formal Methods in System Design, 1992.","DOI":"10.1007\/BF00121125"},{"key":"5_CR13","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0743-1066(92)90047-7","volume":"14","author":"J. Hsiang","year":"1992","unstructured":"Jieh Hsiang, H\u00e9l\u00e8ne Kirchner, and Michael Rusinowitch. The term rewriting approach to automated theorem proving. J. Logic Programming, 14:71\u201399, 1992.","journal-title":"J. Logic Programming"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/0004-3702(85)90074-8","volume":"25","author":"J. Hsiang","year":"1985","unstructured":"Jieh Hsiang. Refutational theorem proving using term-rewriting systems. Artificial Intelligence, 25:255\u2013300, 1985.","journal-title":"Artificial Intelligence"},{"key":"5_CR15","unstructured":"Udo Kebschull. Verhaltensbasierte und spektrale Logiksynthese mehrstufiger Schaltnetze unter Verwendung von Bin\u00e4rb\u00e4umen. PhD thesis, Universit\u00e4t T\u00fcbingen, D, June 1994."},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Udo Kebschull, Endric Schubert, and Wolfgang Rosenstiel. Multilevel logic synthesis based on functional decision diagrams. In Proc. European Design Automation Conference (EURO-DAC), 1992.","DOI":"10.1109\/EDAC.1992.205890"},{"key":"5_CR17","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-1-4612-3658-0_2","volume-title":"Current Trends in Hardware Verification and Automated Theorem Proving","author":"P. Narendran","year":"1989","unstructured":"Paliath Narendran and Jonathan Stillman. Formal verification of the Sobel image processing chip. In Graham Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 92\u2013127. Springer-Verlag, New York, NY, 1989."},{"key":"5_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Proc. 8th Conf. Computer Aided Verication (CAV)","author":"S. Owre","year":"1996","unstructured":"S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. K. Srivas. PVS: Combining specification, proof checking, and model checking. In Rajeev Alur and Thomas A. Henzinger, editors, Proc. 8th Conf. Computer Aided Verication (CAV), LNCS 1102, pages 411\u2013414. Springer, 1996."},{"key":"5_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/3-540-61474-5_63","volume-title":"Computer-Aided Verification, CAV\u2019 96","author":"H. Rue\u00df","year":"1996","unstructured":"H. Rue\u00df, N. Shankar, and M. K. Srivas. Modular verification of SRT division. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV\u2019 96, number 1102 in Lecture Notes in Computer Science, pages 123\u2013134, New Brunswick, NJ, July\/August 1996. Springer-Verlag."},{"key":"5_CR20","unstructured":"D. Russinoff. A mechanically checked proof of IEEE compliance of a register-transfer-level speci, cation of the AMD-K7\u2122 floating-point division and square root instructions. Technical report, 1998. At URL http:\/\/www.onr.com\/user\/russ\/david\/k7-div-sqrt.html ."},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Wilhelm G. Spruth. The design of a microprocessor. Springer, 1989.","DOI":"10.1007\/978-3-642-74916-2"},{"key":"5_CR22","unstructured":"M. Ronan Sleep, M. J. Plasmeijer, and Marko C. J. D. van Eekelen, editors. Term Graph Rewriting: Theory and Practice. John Wiley & Sons, 1993."},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Gunnar St\u00e5lmarck and M. S\u00e4flund. Modelling and verifying systems and software in prepositional logic. In B. K. Daniels, editor, Proc. Safety in Computer Control Systems (SAFECOMP), pages 31\u201336, Gatwick, UK, 1990. Pergamon Press.","DOI":"10.1016\/B978-0-08-040953-5.50011-8"},{"key":"5_CR24","unstructured":"Gunnar St\u00e5lmarck. System for determining prepositional logic theorems by applying values and rules to triplets that are generated from Boolean formula, 1994. United States Patent number 5,276,897; see also Swedish Patent 467 076."},{"key":"5_CR25","unstructured":"Jan van Leeuwen, editor. Handbook of Theoretical Computer Science, volume B (Formal Models and Semantics). Elsevier-The MIT Press, paperback edition, 1994."},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Martin Wirsing. Algebraic specification. In van Leeuwen [vL94], chapter 13, pages 675\u2013788.","DOI":"10.1016\/B978-0-444-88074-1.50018-4"},{"key":"5_CR27","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1006\/jsco.1996.0030","volume":"21","author":"H. Zhang","year":"1996","unstructured":"Hantao Zhang, Maria Paola Bonacina, and Jieh Hsiang. PSATO: a distributed prepositional prover and its application to quasigroup problems. J. Symbolic Computation, 21:543\u2013560, 1996.","journal-title":"J. Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Applied Formal Methods \u2014 FM-Trends 98"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48257-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T20:56:13Z","timestamp":1737320173000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48257-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664628","9783540482574"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-48257-1_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}