{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,26]],"date-time":"2026-08-26T03:57:34Z","timestamp":1787716654236,"version":"build-2784847793"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540008989","type":"print"},{"value":"9783540365778","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_40","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:12:04Z","timestamp":1269882724000},"page":"553-568","source":"Crossref","is-referenced-by-count":204,"title":["Generalized Symbolic Execution for Model Checking and Testing"],"prefix":"10.1007","author":[{"given":"Sarfraz","family":"Khurshid","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Corina S.","family":"P\u0102s\u0102reanu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"40_CR1","doi-asserted-by":"crossref","unstructured":"T. Ball, R. Majumdar, T. Millstein, and S. Rajamani. Automatic predicate abstraction of C programs. In Proc. 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), volume 36-5 of ACM SIGPLAN Notices, pages 203-213. ACM Press, June 2001.","DOI":"10.1145\/378795.378846"},{"key":"40_CR2","doi-asserted-by":"crossref","unstructured":"C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated testing based on Java predicates. In Proc. International Symposium on Software Testing and Analysis (ISSTA), July 2002.","DOI":"10.1145\/566172.566191"},{"issue":"7","key":"40_CR3","doi-asserted-by":"publisher","first-page":"775","DOI":"10.1002\/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H","volume":"30","author":"W. R. Bush","year":"2000","unstructured":"W. R. Bush, J. D. Pincus, and D. J. Sielaff. A static analyzer for finding dynamic programming errors. Software: Practice and Experience, 30(7):775\u2013802, 2000.","journal-title":"Software: Practice and Experience"},{"issue":"4","key":"40_CR4","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: A new symbolic model checker. International Journal on Software Tools for Technology Transfer, 2(4):410\u2013425, 2000.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"40_CR5","doi-asserted-by":"crossref","unstructured":"A. Coen-Porisini, G. Denaro, C. Ghezzi, and M. Pezze. Using symbolic execution for verifying safety-critical systems. In Proc. 8th European Software Engineering Conference held jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 142\u2013151. ACM Press, 2001.","DOI":"10.1145\/503209.503230"},{"key":"40_CR6","doi-asserted-by":"crossref","unstructured":"J. Corbett, M. Dwyer, J. Hatcli., S. Laubach, C. Pasareanu, Robby, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In C. Ghezzi, M. Jazayeri, and A. Wolf, editors, Proc. 22nd International Conference on Software Engineering (ICSE), pages 439\u2013448. ACM, 2000.","DOI":"10.1145\/337180.337234"},{"key":"40_CR7","unstructured":"D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Research Report 159, Compaq Systems Research Center, 1998."},{"key":"40_CR8","doi-asserted-by":"crossref","unstructured":"A. Gargantini and C. Heitmeyer. Using model checking to generate tests from requirements specifications. In Proc. 7th European Engineering Conference held jointly with the 7th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 146\u2013162. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48166-4_10"},{"key":"40_CR9","doi-asserted-by":"crossref","unstructured":"P. Godefroid. Model checking for programming languages using VeriSoft. In Proc. 24th Annual ACM Symposium on the Principles of Programming Languages (POPL), pages 174\u2013186, Paris, France, Jan. 1997.","DOI":"10.1145\/263699.263717"},{"key":"40_CR10","doi-asserted-by":"crossref","unstructured":"A. Groce and W. Visser. Model checking java programs using structural heuristics. In Proc. International Symposium on Software Testing and Analysis (ISSTA). ACM Press, July 2002.","DOI":"10.1145\/566172.566175"},{"key":"40_CR11","doi-asserted-by":"crossref","unstructured":"M. P. E. Heimdahl, Y. Choi, and M. Whalen. Deviation analysis through model checking. In Proc. 17th IEEE International Conference on Automated Software Engineering (ASE), 2002.","DOI":"10.1109\/ASE.2002.1114992"},{"issue":"5","key":"40_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279\u2013294, May 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"40_CR13","doi-asserted-by":"crossref","unstructured":"H. Hong, I. Lee, O. Sokolsky, and H. Ural. A temporal logic based theory of test coverage and generation. In Proc. 8th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Apr. 2002.","DOI":"10.1007\/3-540-46002-0_23"},{"issue":"7","key":"40_CR14","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J. C. King","year":"1976","unstructured":"J. C. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385\u2013394, 1976.","journal-title":"Communications of the ACM"},{"key":"40_CR15","doi-asserted-by":"crossref","unstructured":"A. Moeller and M. I. Schwartzbach. The pointer assertion logic engine. In Proc. SIGPLAN Conference on Programming Languages Design and Implementation (PLDI), Snowbird, UT, June 2001.","DOI":"10.1145\/378795.378851"},{"issue":"8","key":"40_CR16","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"35","author":"W. Pugh","year":"1992","unstructured":"W. Pugh. A Practical Algorithm for Exact Array Dependence Analysis. Communications of the ACM, 35(8):102\u2013114, 1992.","journal-title":"Communications of the ACM"},{"key":"40_CR17","doi-asserted-by":"crossref","unstructured":"M. Sagiv, T. Reps, and R. Wilhelm. Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems, Jan. 1998.","DOI":"10.1145\/271510.271517"},{"key":"40_CR18","doi-asserted-by":"crossref","unstructured":"M. Vaziri and D. Jackson. Checking properties of heap-manipulating procedures with a constraint solver. In Proc. 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Poland, Apr. 2003.","DOI":"10.1007\/3-540-36577-X_37"},{"key":"40_CR19","doi-asserted-by":"crossref","unstructured":"W. Visser, K. Havelund, G. Brat, and S. Park. Model checking programs. In Proc. 15th IEEE International Conference on Automated Software Engineering (ASE), Grenoble, France, 2000.","DOI":"10.1109\/ASE.2000.873645"},{"key":"40_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 9th International Static Analysis Symposium (SAS)","author":"T. Yavuz-Kahveci","year":"2002","unstructured":"T. Yavuz-Kahveci and T. Bultan. Automated verification of concurrent linked lists with counters. In G. P. M. Hermenegildo, editor, Proc. 9th International Static Analysis Symposium (SAS), volume 2477 of Lecture Notes in Computer Science. Springer-Verlag, 2002."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T14:50:44Z","timestamp":1558968644000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_40","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2003]]}}}