{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T10:12:38Z","timestamp":1742379158277},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540304920"},{"type":"electronic","value":"9783540322405"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11589976_3","type":"book-chapter","created":{"date-parts":[[2005,10,26]],"date-time":"2005-10-26T13:38:16Z","timestamp":1130333896000},"page":"20-32","source":"Crossref","is-referenced-by-count":11,"title":["Software Model Checking: Searching for Computations in the Abstract or the Concrete"],"prefix":"10.1007","author":[{"given":"Patrice","family":"Godefroid","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nils","family":"Klarlund","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.: The SLAM Toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 260\u2013264. Springer, Heidelberg (2001)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC lite: A new implementation of the cooperating validity checker category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"3_CR3","volume-title":"Proceedings of ICSE 2004 (26th International Conference on Software Engineering)","author":"D. Beyer","year":"2004","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating Test from Counterexamples. In: Proceedings of ICSE 2004 (26th International Conference on Software Engineering), May 2004. ACM, New York (2004)"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: Proceedings of ISSTA 2002 (International Symposium on Software Testing and Analysis), pp. 123\u2013133 (2002)","DOI":"10.1145\/566171.566191"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: Extracting Finite-State Models from Java Source Code. In: Proceedings of the 22nd International Conference on Software Engineering (2000)","DOI":"10.1145\/337180.337234"},{"key":"3_CR8","volume-title":"Proceedings of ICSE 2005 (27th International Conference on Software Engineering)","author":"C. Csallner","year":"2005","unstructured":"Csallner, C., Smaragdakis, Y.: Check\u2019n Crash: Combining Static Checking and Testing. In: Proceedings of ICSE 2005 (27th International Conference on Software Engineering), May 2005. ACM, New York (2005)"},{"issue":"2\/3","key":"3_CR9","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1023\/B:FORM.0000040028.49845.67","volume":"25","author":"Matthew B. Dwyer","year":"2004","unstructured":"Dwyer, M.B., Hatcliff, J., Prasad, V.R., Robby: Exploiting Object Escape and Locking Information in Partial Order Reduction for Concurrent Object-Oriented Programs. In: Formal Methods in System Design (2004) (to appear)","journal-title":"Formal Methods in System Design"},{"key":"3_CR10","unstructured":"Edvardsson, J.: A Survey on Automatic Test Data Generation. In: Proceedings of the 2nd Conference on Computer Science and Engineering, Linkoping, October 1999, pp. 21\u201328 (1999)"},{"key":"3_CR11","unstructured":"Ernst, M.D.: Static and dynamic analysis: synergy and duality. In: Proceedings of WODA 2003 (ICSE Workshop on Dynamic Analysis), Portland (May 2003)"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic Partial-Order Reduction for Model Checking Software. In: Proceedings of POPL 2005 (32nd ACM Symposium on Principles of Programming Languages), Long beach, January 2005, pp. 110\u2013121 (2005)","DOI":"10.1145\/1040305.1040315"},{"key":"3_CR13","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","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems \u2013 An Approach to the State-Explosion Problem. In: Godefroid, P. (ed.) Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model Checking for Programming Languages using VeriSoft. In: Proceedings of POPL 1997 (24th ACM Symposium on Principles of Programming Languages), Paris, January 1997, pp. 174\u2013186 (1997)","DOI":"10.1145\/263699.263717"},{"key":"3_CR15","unstructured":"Godefroid, P.: The Soundness of Bugs is What Matters (Position Paper). In: Proceedings of BUGS 2005 (PLDI 2005 Workshop on the Evaluation of Software Defect Detection Tools), Chicago (June 2005)"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed Automated Random Testing. In: Proceedings of PLDI 2005 (ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation), Chicago, June 2005, pp. 213\u2013223 (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/3-540-49059-0_28","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"E. Gunter","year":"1999","unstructured":"Gunter, E., Peled, D.: Path Exploration Tool. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 405. Springer, Heidelberg (1999)"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Gupta, N., Mathur, A.P., Soffa, M.L.: Generating test data for branch coverage. In: Proceedings of the 15th IEEE International Conference on Automated Software Engineering, September 2000, pp. 219\u2013227 (2000)","DOI":"10.1109\/ASE.2000.873666"},{"key":"3_CR20","unstructured":"Hastings, R., Joyce, B.: Purify: Fast Detection of Memory Leaks and Access Errors. In: Proceedings of the Usenix Winter 1992 Technical Conference, Berkeley, January 1992, pp. 125\u2013138 (1992)"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Proceedings of the 29th ACM Symposium on Principles of Programming Languages, Portland, January 2002, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Smith, M.H.: A Practical Method for Verifying Event-Driven Software. In: Proceedings of the 21st International Conference on Software Engineering, pp. 597\u2013607 (1999)","DOI":"10.1145\/302405.302710"},{"key":"3_CR23","unstructured":"Ics. web page, http:\/\/www.icansolve.com\/"},{"issue":"7","key":"3_CR24","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic Execution and Program Testing. Journal of the ACM\u00a019(7), 385\u2013394 (1976)","journal-title":"Journal of the ACM"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Korel, B.: A dynamic Approach of Test Data Generation. In: IEEE Conference on Software Maintenance, San Diego, November 1990, pp. 311\u2013317 (1990)","DOI":"10.1109\/ICSM.1990.131379"},{"key":"3_CR26","unstructured":"Larson, E., Austin, T.: High Coverage Detection of Input-Related Security Faults. In: Proceedings of 12th USENIX Security Symposium, D.C (August 2003)"},{"key":"3_CR27","unstructured":"lp_solve. web page, http:\/\/groups.yahoo.com\/group\/lp_solve\/"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Park, D., Chou, A., Engler, D., Dill, D.: CMC: A pragmatic approach to model checking real code. In: Proceedings of OSDI 2002 (2002)","DOI":"10.1145\/1060289.1060297"},{"key":"3_CR29","volume-title":"The Art of Software Testing","author":"G.J. Myers","year":"1979","unstructured":"Myers, G.J.: The Art of Software Testing. Wiley, Chichester (1979)"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Necula, G.C., McPeak, S., Weimer, W.: CCured: Type-Safe Retrofitting of Legacy Code. In: Proceedings of POPL 2002 (29th ACM Symposium on Principles of Programming Languages), Portland, January 2002, pp. 128\u2013139 (2002)","DOI":"10.1145\/565816.503286"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Offutt, J., Hayes, J.: A Semantic Model of Program Faults. In: Proceedings of ISSTA 1996 (International Symposium on Software Testing and Analysis), San Diego, January 1996, pp. 195\u2013200 (1996)","DOI":"10.1145\/229000.226317"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11513988_7","volume-title":"Computer Aided Verification","author":"C. Pasareanu","year":"2005","unstructured":"Pasareanu, C., Pelanek, R., Visser, W.: Concrete Model Checking with Abstract Matching and Refinement. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 52\u201366. Springer, Heidelberg (2005)"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Wu, D.: KISS: Keep It Simple and Sequential. In: Proceedings of PLDI 2004 (ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation), Washington D.C (June 2004)","DOI":"10.1145\/996841.996845"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: A Concolic Unit testing Engine for C. In: Proceedings of FSE 2005 (13th International Symposium on the Foundations of Software Engineering), Lisbon (September 2005)","DOI":"10.1145\/1081706.1081750"},{"key":"3_CR35","unstructured":"Simplify. web page, http:\/\/research.compaq.com\/SRC\/esc\/Simplify.html"},{"issue":"3","key":"3_CR36","first-page":"121","volume":"3","author":"F. Tip","year":"1995","unstructured":"Tip, F.: A survey of program slicing techniques. Journal of Programming Languages\u00a03(3), 121\u2013189 (1995)","journal-title":"Journal of Programming Languages"},{"key":"3_CR37","unstructured":"Valgrind. web page, http:\/\/valgrind.org\/"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model Checking Programs. In: Proceedings of ASE 2000 (15th International Conference on Automated Software Engineering), Grenoble (September 2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Visser, W., Pasareanu, C., Khurshid, S.: Test Input Generation with Java PathFinder. In: Proceedings of ACM SIGSOFT ISSTA 2004 (International Symposium on Software Testing and Analysis), Boston (July 2004)","DOI":"10.1145\/1007512.1007526"},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-540-31980-1_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Xie","year":"2005","unstructured":"Xie, T., Marinov, D., Schulte, W., Notkin, D.: Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a0TACAS 2005, pp. 365\u2013381. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11589976_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T14:06:19Z","timestamp":1586527579000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11589976_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540304920","9783540322405"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/11589976_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}