{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T17:35:30Z","timestamp":1725730530473},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642389153"},{"type":"electronic","value":"9783642389160"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38916-0_5","type":"book-chapter","created":{"date-parts":[[2013,6,9]],"date-time":"2013-06-09T22:13:47Z","timestamp":1370816027000},"page":"76-95","source":"Crossref","is-referenced-by-count":4,"title":["Test Program Generation for a Microprocessor"],"prefix":"10.1007","author":[{"given":"Achim D.","family":"Brucker","sequence":"first","affiliation":[]},{"given":"Abderrahmane","family":"Feliachi","sequence":"additional","affiliation":[]},{"given":"Yakoub","family":"Nemouchi","sequence":"additional","affiliation":[]},{"given":"Burkhart","family":"Wolff","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Appenzeller, D.P., Kuehlmann, A.: Formal verification of a powerpc microprocessor. In: Proceedings of the 1995 IEEE International Conference on Computer Design: VLSI in Computers and Processors, ICCD 1995, pp. 79\u201384 (October 1995), doi:10.1109\/ICCD.1995.528794","DOI":"10.1109\/ICCD.1995.528794"},{"key":"5_CR2","unstructured":"Beyer, S.: Putting it all together - Formal Verification of the VAMP. PhD thesis, Saarland University, Saarbr\u00fccken, Germany (2005)"},{"issue":"4","key":"5_CR3","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/s10009-006-0204-6","volume":"8","author":"S. Beyer","year":"2006","unstructured":"Beyer, S., Jacobi, C., Kr\u00f6ning, D., Leinenbach, D., Paul, W.J.: Putting it all together \u2013 formal verification of the vamp. Int. J. Softw. Tools Technol. Transf.\u00a08(4), 411\u2013430 (2006) ISSN 1433-2779","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Biswas, P., Freeman, A., Yamada, K., Nakagawa, N., Uchiyama, K.: Functional verification of the superscalar sh-4 microprocessor. In: Proceeding of the IEEE Compcon 1997, pp. 115\u2013120 (February 1997), doi:10.1109\/CMPCON.1997.584682","DOI":"10.1109\/CMPCON.1997.584682"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-642-00593-0_28","volume-title":"Fundamental Approaches to Software Engineering","author":"A.D. Brucker","year":"2009","unstructured":"Brucker, A.D., Wolff, B.: HOL TestGen: An interactive test-case generation framework. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503, pp. 417\u2013420. Springer, Heidelberg (2009)"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Brucker, A.D., Wolff, B.: On theorem prover-based testing. Formal Aspects of Computing, FAC (2012), doi:10.1007\/s00165-012-0222-y, ISSN 0934-5043","DOI":"10.1007\/s00165-012-0222-y"},{"key":"5_CR7","unstructured":"Brucker, A.D., Br\u00fcgger, L., Krieger, M.P., Wolff, B.: HOL-TestGen 1.7.0 user guide. Technical Report 1551, Laboratoire en Recherche en Informatique (LRI), Universit\u00e9 Paris-Sud 11, France (April 2012)"},{"key":"5_CR8","unstructured":"Common Criteria. Common criteria for information technology security evaluation (version 3.1), Part 3: Security assurance components (September 2006) Available as document CCMB-2006-09-003"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"5_CR10","unstructured":"Dorrenbacher, J.: Formal Specification and Verification of Microkernel. PhD thesis, Saarland University, Saarbr\u00fccken, Germany (2010)"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Fallah, F., Takayama, K.: A new functional test program generation methodology. In: Proceedings of the 2001 International Conference on Computer Design, ICCD 2001, pp. 76\u201381 (2001), doi:10.1109\/ICCD.2001.955006","DOI":"10.1109\/ICCD.2001.955006"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/10930755_2","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Fox","year":"2003","unstructured":"Fox, A.: Formal specification and verification of arm6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 25\u201340. Springer, Heidelberg (2003)"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Formal verification at intel. In: LICS, pp. 45\u201354. IEEE Computer Society (2003), doi:10.1109\/LICS.2003.1210044, ISBN 0-7695-1884-2","DOI":"10.1109\/LICS.2003.1210044"},{"issue":"3","key":"5_CR14","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1109\/TCAD.1984.1270076","volume":"3","author":"J.P. Hayes","year":"1984","unstructured":"Hayes, J.P.: Fault modeling for digital mos integrated circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a03(3), 200\u2013208 (1984), doi:10.1109\/TCAD.1984.1270076, ISSN 0278-0070","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"5_CR15","volume-title":"Computer Architecture: A Quantitative Approach","author":"J.L. Hennessy","year":"2006","unstructured":"Hennessy, J.L., Patterson, D.A.: Computer Architecture: A Quantitative Approach, 4th edn. Morgan Kaufmann Publishers Inc., San Francisco (2006) ISBN 0123704901","edition":"4"},{"key":"5_CR16","unstructured":"Hilderman, V., Baghai, T.: Avionics Certification: A Complete Guide to DO-178 (Software), DO-254 (Hardware). Avionics Communications Inc. (2007) ISBN 978-1-885544-25-4"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Kamkin, A., Kornykhin, E., Vorobyev, D.: Reconfigurable model-based test program generator for microprocessors. In: IEEE International Conference on Software Testing Verification and Validation Workshop, pp. 47\u201354 (2011), doi:10.1109\/ICSTW.2011.35","DOI":"10.1109\/ICSTW.2011.35"},{"issue":"7","key":"5_CR18","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM\u00a052(7), 107\u2013115 (2009), doi:10.1145\/1538788.1538814, ISSN 0001-0782","journal-title":"Communications of the ACM"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Mishra, P., Dutt, N.: Specification-driven directed test generation for validation of pipelined processors. ACM Trans. Design Autom. Electr. Syst.\u00a013(3) (2008)","DOI":"10.1145\/1367045.1367051"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"1","key":"5_CR21","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1023\/A:1008669628911","volume":"14","author":"D.M. Russinoff","year":"1999","unstructured":"Russinoff, D.M.: A mechanically checked proof of correctness of the amd k5 floating point square root microcode. Formal Methods in System Design\u00a014(1), 75\u2013125 (1999)","journal-title":"Formal Methods in System Design"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Shen, H., Ma, L., Zhang, H.: Crpg: a configurable random test-program generator for microprocessors. In: IEEE International Symposium on Circuits and Systems, ISCAS 2005, vol.\u00a04, pp. 4171\u20134174 (May 2005), doi:10.1109\/ISCAS.2005.1465550","DOI":"10.1109\/ISCAS.2005.1465550"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Srinivasan, S.K., Velev, M.N.: Formal verification of an intel xscale processor model with scoreboarding, specialized execution pipelines, and impress data-memory exceptions. In: MEMOCODE, vol.\u00a07, pp. 65\u201374. IEEE Computer Society (2003), doi:10.1109\/MEMCOD.2003.1210090, ISBN 0-7695-1923-7","DOI":"10.1109\/MEMCOD.2003.1210090"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-540-74591-4_26","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"2007","unstructured":"Wenzel, M., Wolff, B.: Building formal method tools in the Isabelle\/Isar framework. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 352\u2013367. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38916-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T10:21:56Z","timestamp":1578478916000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38916-0_5"}},"subtitle":["A Case-Study"],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642389153","9783642389160"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38916-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}