{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:10:41Z","timestamp":1770293441442,"version":"3.49.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319127354","type":"print"},{"value":"9783319127361","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12736-1_11","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T10:53:24Z","timestamp":1413197604000},"page":"196-215","source":"Crossref","is-referenced-by-count":8,"title":["A Method for Scalable and Precise Bug Finding Using Program Analysis and Model Checking"],"prefix":"10.1007","author":[{"given":"Manuel","family":"Valdiviezo","sequence":"first","affiliation":[]},{"given":"Cristina","family":"Cifuentes","sequence":"additional","affiliation":[]},{"given":"Padmanabhan","family":"Krishnan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T. Ball","year":"2011","unstructured":"Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Communications of the ACM\u00a054, 68\u201376 (2011)","journal-title":"Communications of the ACM"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-27705-4_12","volume-title":"Verified Software: Theories, Tools, Experiments","author":"F. Merz","year":"2012","unstructured":"Merz, F., Falke, S., Sinz, C.: LLBMC: Bounded model checking of C and C++ programs using a compiler IR. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 146\u2013161. Springer, Heidelberg (2012)"},{"key":"11_CR3","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., Kroning, 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":"11_CR4","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Hongjun, Z.: Bandera: Extracting finite-state models from Java source code. In: Proceedings of the International Conference on Software Engineering, pp. 439\u2013448 (2000)","DOI":"10.1145\/337180.337234"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: Proceedings of the Conference on Programming Language Design and Implementation (PLDI), pp. 57\u201368. ACM Press (June 2002)","DOI":"10.1145\/543552.512538"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Dor, N., Adams, S., Das, M., Yang, Z.: Software validation via scalable path-sensitive value flow analysis. In: Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), pp. 12\u201322. ACM (2004)","DOI":"10.1145\/1013886.1007515"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Jung, Y., Yi, K.: Practical memory leak detector based on parameterized procedural summaries. In: Proceedings of the 7th International Symposium on Memory Management (ISMM), pp. 131\u2013140 (2008)","DOI":"10.1145\/1375634.1375653"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Sui, Y., Ye, D., Xue, J.: Static memory leak detection using full-sparse value-flow analysis. In: Proceedings of the 2012 International Symposium on Software Testing and Analysis (ISSTA), pp. 254\u2013264. ACM (2012)","DOI":"10.1145\/2338965.2336784"},{"key":"11_CR9","series-title":"IFIP AICT","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-15240-5_10","volume-title":"Theoretical Computer Science","author":"N. Yatapanage","year":"2010","unstructured":"Yatapanage, N., Winter, K., Zafar, S.: Slicing behavior tree models for verification. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IFIP AICT, vol.\u00a0323, pp. 125\u2013139. Springer, Heidelberg (2010)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Park, M., Byun, T., Choi, Y.: Property-based code slicing for efficient verification of OSEK\/VDX operating systems. In: Proceedings of the First International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), pp. 69\u201384 (2012)","DOI":"10.4204\/EPTCS.105.6"},{"issue":"2","key":"11_CR11","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1016\/j.infsof.2009.10.004","volume":"52","author":"Y. Kim","year":"2010","unstructured":"Kim, Y., Lee, J., Han, H., Choe, K.M.: Filtering false alarms of buffer overflow analysis using SMT solvers. Information and Software Technology\u00a052(2), 210\u2013219 (2010)","journal-title":"Information and Software Technology"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Chebaro, O., Kosmatov, N., Giorgetti, A., Julliand, J.: Program slicing enhances a verification technique combining static and dynamic analysis. In: Proceedings of the ACM Symposium on Applied Computing (SAC), pp. 1284\u20131291 (2012)","DOI":"10.1145\/2245276.2231980"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"issue":"4","key":"11_CR14","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R. Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems\u00a013(4), 451\u2013490 (1991)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Hampapuram, H., Yang, Y., Das, M.: Symbolic path simulation in path-sensitive dataflow analysis. In: Proceeding of PASTE, pp. 52\u201358. ACM Press (2005)","DOI":"10.1145\/1108768.1108808"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Cifuentes, C., Keynes, N., Li, L., Hawes, N., Valdiviezo, M., Browne, A., Zimmermann, J., Craik, A., Teoh, D., Hoermann, C.: Static deep error checking in large system applications using Parfait. In: Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering, pp. 432\u2013435. ACM (2011)","DOI":"10.1145\/2025113.2025183"},{"key":"11_CR17","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional (2011)"},{"key":"11_CR18","unstructured":"Anderson, P.: The use and limitations of static-analysis tools to improve software quality. CrossTalk: The Journal of Defense Software Engineering, 18\u201321 (2008)"},{"key":"11_CR19","unstructured":"NIST: National Institute of Standards and Technology SAMATE Reference Dataset (SRD) project (January 2006), \n                    \n                      http:\/\/samate.nist.gov\/SRD"},{"issue":"15","key":"11_CR20","doi-asserted-by":"publisher","first-page":"1885","DOI":"10.1002\/cpe.1036","volume":"18","author":"G.R. Luecke","year":"2006","unstructured":"Luecke, G.R., Coyle, J., Hoekstra, J., Kraeva, M., Li, Y., Taborskaia, O., Wang, Y.: A survey of systems for detecting serial run-time errors. Concurrency and Computation \u2013 Practice and Experience\u00a018(15), 1885\u20131907 (2006)","journal-title":"Concurrency and Computation \u2013 Practice and Experience"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12736-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T00:17:03Z","timestamp":1559002623000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-12736-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319127354","9783319127361"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12736-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}