{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:11:28Z","timestamp":1763467888637},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540878728"},{"type":"electronic","value":"9783540878735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-87873-5_19","type":"book-chapter","created":{"date-parts":[[2008,9,25]],"date-time":"2008-09-25T12:04:10Z","timestamp":1222344250000},"page":"225-239","source":"Crossref","is-referenced-by-count":15,"title":["Formal Functional Verification of Device Drivers"],"prefix":"10.1007","author":[{"given":"Eyad","family":"Alkassar","sequence":"first","affiliation":[]},{"given":"Mark A.","family":"Hillebrand","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-540-77966-7_14","volume-title":"Hardware and Software: Verification and Testing","author":"M.A. Hillebrand","year":"2008","unstructured":"Hillebrand, M.A., Paul, W.: On the architecture of system verification environments. In: Yorav, K. (ed.) HVC 2007. LNCS, vol.\u00a04899, pp. 153\u2013168. Springer, Heidelberg (2008)"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"19_CR3","unstructured":"American National Standards Institute: ANSI NCITS 340-2000: AT Attachment-5 with Packet Interface (2000)"},{"key":"19_CR4","first-page":"309","volume-title":"ICCD 2005","author":"M. Hillebrand","year":"2005","unstructured":"Hillebrand, M., In der Rieden, T., Paul, W.: Dealing with I\/O devices in the context of pervasive system verification. In: ICCD 2005, pp. 309\u2013316. IEEE Computer Society, Los Alamitos (2005)"},{"key":"19_CR5","unstructured":"Alkassar, E., et al.: Formal device and programming model for a serial interface. In: Beckert, B. (ed.) VERIFY 2007, pp. 4\u201320 (2007)"},{"key":"19_CR6","first-page":"433","volume-title":"ICCAD","author":"G. Berry","year":"2003","unstructured":"Berry, G., Kishinevsky, M., Singh, S.: System level design and verification using a synchronous language. In: ICCAD, pp. 433\u2013440. IEEE Computer Society \/ ACM, Los Alamitos (2003)"},{"key":"19_CR7","volume-title":"System-on-a-Chip Verification: Methodology and Techniques","author":"P. Rashinkar","year":"2001","unstructured":"Rashinkar, P., Paterson, P., Singh, L.: System-on-a-Chip Verification: Methodology and Techniques. Kluwer Academic Publishers, Norwell (2001)"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 103\u2013122. Springer, Heidelberg (2001)"},{"key":"19_CR9","unstructured":"Microsoft Corporation: SDV: Static driver verifier (2004), \n                    \n                      http:\/\/www.microsoft.com\/whdc\/devtools\/tools\/sdv.mspx"},{"key":"19_CR10","volume-title":"ICFP","author":"T. Hallgren","year":"2005","unstructured":"Hallgren, T., et al.: A principled approach to operating system construction in Haskell. In: Danvy, O., Pierce, B.C. (eds.) ICFP. ACM, New York (2005)"},{"issue":"4","key":"19_CR11","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/1278901.1278904","volume":"41","author":"G. Heiser","year":"2007","unstructured":"Heiser, G., et al.: Towards trustworthy computing systems: Taking microkernels to the next level. SIGOPS Oper. Syst. Rev.\u00a041(4), 3\u201311 (2007)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"19_CR12","unstructured":"The FLINT Project, \n                    \n                      http:\/\/flint.cs.yale.edu\/flint\/"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"Symposium on 25 years of Model Checking","author":"G.J. Holzmann","year":"2006","unstructured":"Holzmann, G.J.: New challenges in model checking. In: Symposium on 25 years of Model Checking, Seattle, USA, LNCS, vol.\u00a04925. Springer, Heidelberg (August 2006)"},{"key":"19_CR14","first-page":"3","volume-title":"ICECCS","author":"L. Freitas","year":"2007","unstructured":"Freitas, L., Fu, Z., Woodcock, J.: POSIX file store in Z\/Eves: An experiment in the verified software repository. In: ICECCS, pp. 3\u201314. IEEE Computer Society, Los Alamitos (2007)"},{"key":"19_CR15","first-page":"251","volume-title":"ICECCS","author":"A. Butterfield","year":"2007","unstructured":"Butterfield, A., Woodcock, J.: Formalising Flash memory: First steps. In: ICECCS, pp. 251\u2013260. IEEE Computer Society, Los Alamitos (2007)"},{"issue":"12","key":"19_CR16","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"R.J. Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Commun. ACM\u00a018(12), 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/BFb0055631","volume-title":"CONCUR 1998","author":"E. Cohen","year":"1998","unstructured":"Cohen, E., Lamport, L.: Reduction in TLA. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 317\u2013331. Springer, Heidelberg (1998)"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/10722010_4","volume-title":"Mathematics of Program Construction","author":"E. Cohen","year":"2000","unstructured":"Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 45\u201359. Springer, Heidelberg (2000)"},{"issue":"3","key":"19_CR19","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10703-006-0003-4","volume":"28","author":"S.D. Stoller","year":"2006","unstructured":"Stoller, S.D., Cohen, E.: Optimistic synchronization-based state-space reduction. Form. Methods Syst. Des.\u00a028(3), 263\u2013289 (2006)","journal-title":"Form. Methods Syst. Des."},{"key":"19_CR20","unstructured":"Tverdyshev, S., Shadrin, A.: Formal verification of gate-level computer systems. In: Rozier, K.Y. (ed.) LFM 2008. NASA STI, NASA, pp. 56\u201358 (2008)"},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"Yu, D., Shao, Z.: Verification of safety properties for concurrent assembly code. In: ICFP 2004 (September 2004)","DOI":"10.21236\/ADA436482"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-540-78800-3_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Alkassar","year":"2008","unstructured":"Alkassar, E., Schirmer, N., Starostin, A.: Formal pervasive verification of a paging mechanism. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 109\u2013123. Springer, Heidelberg (2008)"},{"key":"19_CR23","series-title":"ENTCS","first-page":"23","volume-title":"SSV 2008","author":"D. Leinenbach","year":"2008","unstructured":"Leinenbach, D., Petrova, E.: Pervasive compiler verification \u2013 From verified programs to verified systems. In: SSV 2008. ENTCS, vol.\u00a0217, pp. 23\u201340. Elsevier Science B.V, Amsterdam (2008)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87873-5_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:50:45Z","timestamp":1619524245000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-87873-5_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540878728","9783540878735"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87873-5_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}