{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T06:55:45Z","timestamp":1747810545545},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642050886"},{"type":"electronic","value":"9783642050893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-05089-3_48","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T22:31:40Z","timestamp":1257287500000},"page":"757-772","source":"Crossref","is-referenced-by-count":8,"title":["An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method"],"prefix":"10.1007","author":[{"given":"Danhua","family":"Shao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sarfraz","family":"Khurshid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dewayne E.","family":"Perry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"48_CR1","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated Testing Based on Java Predicates. In: Proc. of ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA (2002)","DOI":"10.1145\/566172.566191"},{"key":"48_CR2","doi-asserted-by":"crossref","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P., Dill, D., Engler, D.: EXE: Automatically Generating Inputs of Death. In: Proc. of the 13th ACM Conference on Computer and Communications Security (CCS) (2006)","DOI":"10.1145\/1180405.1180445"},{"key":"48_CR3","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: Proc. of International Conference on Software Engineering, ICSE (2000)","DOI":"10.1145\/337180.337234"},{"key":"48_CR4","doi-asserted-by":"crossref","unstructured":"Darga, P., Boyapati, C.: Efficient software model checking of data structure properties. In: Proc. of the International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA (2006)","DOI":"10.1145\/1167473.1167504"},{"key":"48_CR5","doi-asserted-by":"crossref","unstructured":"Dennis, G., Chang, F.S.H., Jackson, D.: Modular verification of code with SAT. In: Proc. of the International Symposium on Software Testing and Analysis, ISSTA (2006)","DOI":"10.1145\/1146238.1146251"},{"key":"48_CR6","doi-asserted-by":"crossref","unstructured":"Dolby, J., Vaziri, M., Tip, F.: Finding Bugs Efficiently with a SAT Solver. In: Proc. of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC\/FSE (2007)","DOI":"10.1145\/1287624.1287653"},{"key":"48_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"48_CR8","doi-asserted-by":"crossref","unstructured":"Frias, M.F., Galeotti, J.P., L\u00f3pez Pombo, C.G., Aguirre, N.M.: DynAlloy: upgrading alloy with actions. In: Proc. of International Conference on Software Engineering, ICSE (2005)","DOI":"10.1145\/1062455.1062535"},{"key":"48_CR9","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model Checking for Programming Languages using VeriSoft. In: Proc.of ACM Symposium on Principles of Programming Languages, POPL (1997)","DOI":"10.1145\/263699.263717"},{"key":"48_CR10","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: Proc. of ACM SIGPLAN conference on Programming language design and implementation, PLDI (2005)","DOI":"10.1145\/1065010.1065036"},{"issue":"11","key":"48_CR11","doi-asserted-by":"publisher","first-page":"927","DOI":"10.1109\/32.730543","volume":"24","author":"C. Heitmeyer","year":"1998","unstructured":"Heitmeyer, C., James Kirby, J., Labaw, B., Archer, M., Bharadwaj, R.: Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Transactions on Software Engineering\u00a024(11), 927\u2013948 (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"48_CR12","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"48_CR13","doi-asserted-by":"crossref","unstructured":"Jackson, D.: Automating first-order relational logic. In: Proc. of the International Symposium on Foundations of Software Engineering, FSE (2000)","DOI":"10.1145\/355045.355063"},{"key":"48_CR14","volume-title":"Software Abstractions: logic, language, and analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: logic, language, and analysis. MIT Press, Cambridge (2006)"},{"key":"48_CR15","doi-asserted-by":"crossref","unstructured":"Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: Proc. of the International Symposium on Software Testing and Analysis, ISSTA (2000)","DOI":"10.1145\/347324.383378"},{"key":"48_CR16","doi-asserted-by":"crossref","unstructured":"Khurshid, S., Marinov, D.: TestEra: Specification-based Testing of Java Programs Using SAT. Automated Software Engineering Journal\u00a011(4) (October 2004)","DOI":"10.1023\/B:AUSE.0000038938.10589.b9"},{"key":"48_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Khurshid","year":"2003","unstructured":"Khurshid, S., Pasareanu, C., Visser, W.: Generalized Symbolic Execution for Model Checking and Testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 553\u2013568. Springer, Heidelberg (2003)"},{"key":"48_CR18","doi-asserted-by":"crossref","unstructured":"King, J.C.: Symbolic execution and program testing. Communications of the ACM\u00a019(7) (July 1976)","DOI":"10.1145\/360248.360252"},{"key":"48_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/3-540-44674-5_15","volume-title":"Implementation and Application of Automata","author":"N. Klarlund","year":"2001","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Yu, S., P\u0103un, A. (eds.) CIAA 2000. LNCS, vol.\u00a02088, p. 182. Springer, Heidelberg (2001)"},{"key":"48_CR20","unstructured":"Kuncak, V.: Modular Data Structure Verification. Ph.D. thesis, EECS Department, Massachusetts Institute of Technology (2007)"},{"key":"48_CR21","series-title":"Lecture Notes in Computer Science","first-page":"337","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Leonardo","year":"2008","unstructured":"Leonardo, M., 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":"48_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"48_CR23","unstructured":"Millett, L.I., Teitelbaum, T.: Slicing Promela and its applications to model checking. In: Proc. of the 4th International SPIN Workshop (1998)"},{"key":"48_CR24","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. of 39th Design Automation Conference, DAC (2001)","DOI":"10.1145\/378239.379017"},{"issue":"3","key":"48_CR25","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"48_CR26","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C. In: Proc. of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, ESEC\/FSE (2005)","DOI":"10.1145\/1081706.1081750"},{"issue":"3","key":"48_CR27","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":"48_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A Relational Model Finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"key":"48_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/3-540-36577-X_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Vaziri","year":"2003","unstructured":"Vaziri, M., Jackson, D.: Checking properties of heap-manipulating procedures with a constraint solver. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 505\u2013520. Springer, Heidelberg (2003)"},{"key":"48_CR30","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. In: Proc. of International Conference on Automated Software Engineering, ASE (2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"48_CR31","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Saturn: A scalable framework for error detection using boolean satisfiability. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a029(3) (2007)","DOI":"10.1145\/1232420.1232423"}],"container-title":["Lecture Notes in Computer Science","FM 2009: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-05089-3_48.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:41Z","timestamp":1606186061000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05089-3_48"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050886","9783642050893"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05089-3_48","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}