{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T11:10:09Z","timestamp":1746097809907,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642540127"},{"type":"electronic","value":"9783642540134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54013-4_9","type":"book-chapter","created":{"date-parts":[[2014,1,3]],"date-time":"2014-01-03T01:08:09Z","timestamp":1388711289000},"page":"142-160","source":"Crossref","is-referenced-by-count":8,"title":["Cascade 2.0"],"prefix":"10.1007","author":[{"given":"Wei","family":"Wang","sequence":"first","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of Design Automation Conference (DAC 1999), vol.\u00a0317, pp. 226\u2013320 (1999)","DOI":"10.21236\/ADA360973"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-22438-6_15","volume-title":"Automated Deduction \u2013 CADE-23","author":"S. B\u00f6hme","year":"2011","unstructured":"B\u00f6hme, S., Moskal, M.: Heaps and data structures: A challenge for automated provers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 177\u2013191. Springer, Heidelberg (2011)"},{"key":"9_CR5","first-page":"351","volume":"2","author":"D. Brand","year":"1978","unstructured":"Brand, D., Joyner, W.H.: Verification of protocols using symbolic execution. Comput. Networks\u00a02, 351 (1978)","journal-title":"Comput. Networks"},{"key":"9_CR6","first-page":"23","volume":"7","author":"R.M. Burstall","year":"1972","unstructured":"Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. Machine Intelligence\u00a07, 23\u201350 (1972)","journal-title":"Machine Intelligence"},{"key":"9_CR7","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proc. OSDI 2008, pp. 209\u2013224 (2008)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-71209-1_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Chatterjee","year":"2007","unstructured":"Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamari\u0107, Z.: A reachability predicate for analyzing low-level software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 19\u201333. Springer, Heidelberg (2007)"},{"key":"9_CR9","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":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"9_CR11","first-page":"85","volume":"254","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A precise yet efficient memory model for c. ENTCS\u00a0254, 85\u2013103 (2009)","journal-title":"ENTCS"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ansi-c software. In: ASE, pp. 137\u2013148 (2009)","DOI":"10.1109\/ASE.2009.63"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-c a software analysis perspective (2012)","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., 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":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Programming Language Design and Implementation (PLDI), pp. 234\u2013245 (2002)","DOI":"10.1145\/543552.512558"},{"key":"9_CR17","unstructured":"Grimm, R.: Rats!, a parser generator supporting extensible syntax (2009)"},{"key":"9_CR18","first-page":"226","volume":"385","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Communications of the ACM\u00a0385, 226\u2013394 (1976)","journal-title":"Communications of the ACM"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the future. Revisting precise program verification using SMT solvers. In: POPL, pp. 171\u2013182 (2008)","DOI":"10.1145\/1328897.1328461"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-31424-7_32","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2012","unstructured":"Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 427\u2013443. Springer, Heidelberg (2012)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-540-69738-1_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Z. Rakamari\u0107","year":"2007","unstructured":"Rakamari\u0107, Z., Bingham, J.D., Hu, A.J.: An inference-rule-based decision procedure for verification of heap-manipulating programs with mutable data and cyclic data structures. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 106\u2013121. Springer, Heidelberg (2007)"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-540-93900-9_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Z. Rakamari\u0107","year":"2009","unstructured":"Rakamari\u0107, Z., Hu, A.J.: A scalable memory model for low-level code. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 290\u2013304. Springer, Heidelberg (2009)"},{"key":"9_CR23","unstructured":"Sankaranarayanan, S.: Necla static analysis benchmarks (2009)"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/11817963_17","volume-title":"Computer Aided Verification","author":"N. Sethi","year":"2006","unstructured":"Sethi, N., Barrett, C.W.: Cascade: C assertion checker and deductive engine. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 166\u2013169. Springer, Heidelberg (2006)"},{"key":"9_CR25","doi-asserted-by":"publisher","first-page":"4","DOI":"10.2168\/LMCS-4(4:1)2008","volume":"4","author":"V. Sofronie-Stokkermans","year":"2008","unstructured":"Sofronie-Stokkermans, V.: Interpolation in local theory extensions. Logical Methods in Computer Science\u00a04, 4 (2008)","journal-title":"Logical Methods in Computer Science"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Steensgaard, B.: Points-to analysis in almost linear time. In: ACM Symposium on Principles of Programming Languages, pp. 32\u201341 (1996)","DOI":"10.1145\/237721.237727"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p. 29 (2001)","DOI":"10.1109\/LICS.2001.932480"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Totla, N., Wies, T.: Complete instantiation-based interpolation. In: POPL (2013)","DOI":"10.1145\/2429069.2429132"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-642-27705-4_9","volume-title":"Verified Software: Theories, Tools, Experiments","author":"M. Vujo\u0161evi\u0107-Jani\u010di\u0107","year":"2012","unstructured":"Vujo\u0161evi\u0107-Jani\u010di\u0107, M., Kuncak, V.: Development and evaluation of LAV: An SMT-based error finding platform. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 98\u2013113. Springer, Heidelberg (2012)"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Zitser, M., Lippmann, R., Leek, T.: Testing static analysis tools using exploitable buffer overflows from open source code. SIGSOFT Softw. Eng., 29 (2004)","DOI":"10.1145\/1041685.1029911"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54013-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T10:40:06Z","timestamp":1746096006000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54013-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642540127","9783642540134"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54013-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}