{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:46:44Z","timestamp":1770281204194,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540787990","type":"print"},{"value":"9783540788003","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78800-3_27","type":"book-chapter","created":{"date-parts":[[2008,4,2]],"date-time":"2008-04-02T04:26:19Z","timestamp":1207110379000},"page":"351-366","source":"Crossref","is-referenced-by-count":105,"title":["RWset: Attacking Path Explosion in Constraint-Based Test Generation"],"prefix":"10.1007","author":[{"given":"Peter","family":"Boonstoppel","sequence":"first","affiliation":[]},{"given":"Cristian","family":"Cadar","sequence":"additional","affiliation":[]},{"given":"Dawson","family":"Engler","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: EuroSys (April 2006)","DOI":"10.1145\/1217935.1217943"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_7","volume-title":"SPIN Model Checking and Software Verification","author":"T. Ball","year":"2000","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, Springer, Heidelberg (2000)"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/11537328_2","volume-title":"Model Checking Software","author":"C. Cadar","year":"2005","unstructured":"Cadar, C., Engler, D.: Execution generated test cases: How to make systems code crash itself. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol.\u00a03639, pp. 2\u201323. Springer, Heidelberg (2005)"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P., Dill, D., Engler, D.: EXE: Automatically generating inputs of death. In: Proceedings of the 13th ACM Conference on Computer and Communications Security (October-November 2006)","DOI":"10.1145\/1180405.1180445"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V. Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 519\u2013531. Springer, Heidelberg (2007)"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol.\u00a01032. Springer, New York (1996)"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Compositional dynamic test generation. In: Proceedings of the 34th Symposium on Principles of Programming Languages (POPL 2007) (January 2007)","DOI":"10.1145\/1190216.1190226"},{"key":"27_CR8","volume-title":"Proceedings of the Conference on Programming Language Design and Implementation (PLDI)","author":"P. Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: Proceedings of the Conference on Programming Language Design and Implementation (PLDI), Chicago, IL USA, ACM Press, New York (June 2005)"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Hallem, S., Chelf, B., Xie, Y., Engler, D.: A system and language for building system-specific, static analyses (2002)","DOI":"10.21236\/ADA419593"},{"key":"27_CR10","unstructured":"Herder, J.N.: Towards a true microkernel operating system. Master\u2019s thesis, Vrije Universiteit Amsterdam (2005)"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: The engineering of a model checker: The Gnu i-protocol case study revisited (1999)","DOI":"10.1007\/3-540-48234-2_18"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Lewis, M., Jones, M.: A dead variable analysis for explicit model checking. In: In Proceedings of the ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program (2006)","DOI":"10.1145\/1111542.1111551"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Sen, K.: Hybrid concolic testing. In: Proceedings of the 29th International Conference on Software Engineering (ICSE 2007) (May 2007)","DOI":"10.1109\/ICSE.2007.41"},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C. In: In 5th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE 2005) (September 2005)","DOI":"10.1145\/1081706.1081750"},{"key":"27_CR15","unstructured":"Swift, M.M., Annamalai, M., Bershad, B.N., Levy, H.M.: Recovering device drivers. In: OSDI, pp. 1\u201316 (December 2004)"},{"key":"27_CR16","volume-title":"Operating Systems Design and Implementation","author":"A.S. Tanenbaum","year":"2006","unstructured":"Tanenbaum, A.S., Woodhull, A.S.: Operating Systems Design and Implementation, 3rd edn. Prentice Hall, Englewood Cliffs (2006)","edition":"3"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1007\/3-540-60385-9_13","volume-title":"Correct Hardware Design and Verification Methods","author":"U. Stern","year":"1995","unstructured":"Stern, U., Dill, D.L.: Improved Probabilistic Verification by Hash Compaction. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987, pp. 206\u2013224. Springer, Heidelberg (1995)"},{"key":"27_CR18","unstructured":"Yang, J., Twohey, P., Engler, D., Musuvathi, M.: Using model checking to find serious file system errors (December 2004)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78800-3_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:22:48Z","timestamp":1619508168000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78800-3_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540787990","9783540788003"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78800-3_27","relation":{},"subject":[]}}