{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T15:51:22Z","timestamp":1778082682737,"version":"3.51.4"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319216898","type":"print"},{"value":"9783319216904","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_20","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T06:08:27Z","timestamp":1436940507000},"page":"343-361","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":225,"title":["The SeaHorn Verification Framework"],"prefix":"10.1007","author":[{"given":"Arie","family":"Gurfinkel","sequence":"first","affiliation":[]},{"given":"Temesghen","family":"Kahsai","sequence":"additional","affiliation":[]},{"given":"Anvesh","family":"Komuravelli","sequence":"additional","affiliation":[]},{"given":"Jorge A.","family":"Navas","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-642-33125-1_21","volume-title":"Static Analysis","author":"A Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: Craig interpretation. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 300\u2013316. Springer, Heidelberg (2012)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-27940-9_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: Whale: an interpolation-based algorithm for inter-procedural verification. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 39\u201355. Springer, Heidelberg (2012)"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/978-3-642-36742-7_52","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Albarghouthi","year":"2013","unstructured":"Albarghouthi, A., Gurfinkel, A., Li, Y., Chaki, S., Chechik, M.: UFO: verification with interpolants and abstract interpretation. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 637\u2013640. Springer, Heidelberg (2013)"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1007\/978-3-642-31424-7_48","volume-title":"Computer Aided Verification","author":"A Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: a framework for abstraction- and interpolation-based software verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 672\u2013678. Springer, Heidelberg (2012)"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-642-38856-9_4","volume-title":"Static Analysis","author":"G Amato","year":"2013","unstructured":"Amato, G., Scozzari, F.: Localizing widening and narrowing. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 25\u201342. Springer, Heidelberg (2013)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-319-06200-6_27","volume-title":"NASA Formal Methods","author":"S Arlt","year":"2014","unstructured":"Arlt, S., Rubio-Gonz\u00e1lez, C., R\u00fcmmer, P., Sch\u00e4f, M., Shankar, N.: The gradual verifier. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 313\u2013327. Springer, Heidelberg (2014)"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25\u201332 (2009)","DOI":"10.1109\/FMCAD.2009.5351147"},{"issue":"5\u20136","key":"20_CR8","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker blast. STTT 9(5\u20136), 505\u2013525 (2007)","journal-title":"STTT"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011)"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/978-3-662-46081-8_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A.: Property directed polyhedral abstraction. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 263\u2013281. Springer, Heidelberg (2015)"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., McMillan, K.L., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: SMT, pp. 3\u201311 (2012)","DOI":"10.29007\/1l7f"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-38856-9_8","volume-title":"Static Analysis","author":"N Bj\u00f8rner","year":"2013","unstructured":"Bj\u00f8rner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 105\u2013125. Springer, Heidelberg (2013)"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-31424-7_4","volume-title":"Computer Aided Verification","author":"AR Bradley","year":"2012","unstructured":"Bradley, A.R.: IC3 and beyond: incremental, inductive verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 4\u20134. Springer, Heidelberg (2012)"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/978-3-319-10431-7_20","volume-title":"Software Engineering and Formal Methods","author":"G Brat","year":"2014","unstructured":"Brat, G., Navas, J.A., Shi, N., Venet, A.: IKOS: a framework for static analysis based on abstract interpretation. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 271\u2013277. Springer, Heidelberg (2014)"},{"key":"20_CR15","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. 4424, pp. 19\u201333. Springer, Heidelberg (2007)"},{"key":"20_CR16","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. 2988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: Vcc: A practical system for verifying concurrent c. In: TPHOL. pp. 23\u201342 (2009)","DOI":"10.1007\/978-3-642-03359-9_2"},{"issue":"4","key":"20_CR18","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1109\/TSE.2011.59","volume":"38","author":"L Cordeiro","year":"2012","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: Smt-based bounded model checking for embedded ANSI-C software. IEEE Trans. Softw. Eng. 38(4), 957\u2013974 (2012)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"20_CR19","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the second international symposium on Programming, Paris, France. pp. 106\u2013130 (1976)"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233\u2013247. Springer, Heidelberg (2012)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/978-3-642-54862-8_47","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Angelis De","year":"2014","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: VeriMAP: a tool for verifying programs through transformations. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 568\u2013574. Springer, Heidelberg (2014)"},{"key":"20_CR22","unstructured":"DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical report MSR-TR-2005-70, Microsoft Research (2005)"},{"issue":"4\u2014-5","key":"20_CR23","first-page":"593","volume":"13","author":"G Gange","year":"2013","unstructured":"Gange, G., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: Failure tabled constraint logic programming by interpolation. TPLP 13(4\u2014-5), 593\u2013607 (2013)","journal-title":"TPLP"},{"key":"20_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-642-38088-4_10","volume-title":"NASA Formal Methods","author":"P-L Garoche","year":"2013","unstructured":"Garoche, P.-L., Kahsai, T., Tinelli, C.: Incremental invariant generation using logic-based automatic abstract transformers. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 139\u2013154. Springer, Heidelberg (2013)"},{"key":"20_CR25","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1080\/00207168908803778","volume":"30","author":"P Granger","year":"1989","unstructured":"Granger, P.: Static analysis of arithmetical congruences. Int. J. Comput. Math. 30, 165\u2013190 (1989)","journal-title":"Int. J. Comput. Math."},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI, pp. 405\u2013416 (2012)","DOI":"10.1145\/2345156.2254112"},{"issue":"6","key":"20_CR27","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/s10009-010-0162-x","volume":"12","author":"A Gurfinkel","year":"2010","unstructured":"Gurfinkel, A., Chaki, S.: Combining predicate and numeric abstraction for software model checking. STTT 12(6), 409\u2013427 (2010)","journal-title":"STTT"},{"key":"20_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-20398-5_11","volume-title":"NASA Formal Methods","author":"A Gurfinkel","year":"2011","unstructured":"Gurfinkel, A., Chaki, S., Sapra, S.: Efficient predicate abstraction of program summaries. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 131\u2013145. Springer, Heidelberg (2011)"},{"key":"20_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/978-3-662-46681-0_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Navas, J.A.: SeaHorn: a framework for verifying C programs (Competition Contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 447\u2013450. Springer, Heidelberg (2015)"},{"key":"20_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-88387-6_9","volume-title":"Automated Technology for Verification and Analysis","author":"A Gurfinkel","year":"2008","unstructured":"Gurfinkel, A., Wei, O., Chechik, M.: Model checking recursive programs with exact predicate abstraction. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 95\u2013110. Springer, Heidelberg (2008)"},{"key":"20_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/978-3-642-36742-7_53","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Christ, J., Dietsch, D., Ermis, E., Hoenicke, J., Lindenmann, M., Nutz, A., Schilling, C., Podelski, A.: Ultimate automizer with SMTInterpol. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 641\u2013643. Springer, Heidelberg (2013)"},{"key":"20_CR32","doi-asserted-by":"crossref","unstructured":"Hermenegildo, M.V., Puebla, G., Bueno, F., L\u00f3pez-Garc\u00eda, P.: Program development using abstract interpretation (and the ciao system preprocessor). In: SAS, pp. 127\u2013152 (2003)","DOI":"10.1007\/3-540-44898-5_8"},{"key":"20_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157\u2013171. Springer, Heidelberg (2012)"},{"key":"20_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1007\/978-3-642-31424-7_61","volume-title":"Computer Aided Verification","author":"J Jaffar","year":"2012","unstructured":"Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: TRACER: a symbolic execution tool for verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 758\u2013766. Springer, Heidelberg (2012)"},{"key":"20_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/978-3-319-08867-9_2","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2014","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17\u201334. Springer, Heidelberg (2014)"},{"key":"20_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"846","DOI":"10.1007\/978-3-642-39799-8_59","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2013","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 846\u2013862. Springer, Heidelberg (2013)"},{"key":"20_CR37","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S.: A program transformation for faster goal-directed search. In: FMCAD, pp. 147\u2013154 (2014)","DOI":"10.1109\/FMCAD.2014.6987607"},{"key":"20_CR38","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO, pp. 75\u201388 (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"20_CR39","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.S.: Automatic pool allocation: improving performance by controlling data structure layout in the heap. In: PLDI, pp. 129\u2013142 (2005)","DOI":"10.1145\/1064978.1065027"},{"key":"20_CR40","unstructured":"McMillan, K., Rybalchenko, A.: Solving constrained horn clauses using interpolation. Technical report MSR-TR-2013-6 (2013)"},{"key":"20_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-78769-3_11","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M M\u00e9ndez-Lojo","year":"2008","unstructured":"M\u00e9ndez-Lojo, M., Navas, J., Hermenegildo, M.V.: A flexible, (C)LP-based approach to the analysis of object-oriented programs. In: King, A. (ed.) LOPSTR 2007. LNCS, vol. 4915, pp. 154\u2013168. Springer, Heidelberg (2008)"},{"key":"20_CR42","doi-asserted-by":"crossref","unstructured":"Merz, F., Falke, S., Sinz, C.: LLBMC: bounded model checking of C and C++programs using a compiler IR. In: VSTTE. pp. 146\u2013161 (2012)","DOI":"10.1007\/978-3-642-27705-4_12"},{"key":"20_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-45789-5_11","volume-title":"Static Analysis","author":"A Min\u00e9","year":"2002","unstructured":"Min\u00e9, A.: A few graph-based relational numerical abstract domains. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 117\u2013132. Springer, Heidelberg (2002)"},{"issue":"1","key":"20_CR44","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. High. Order Symb. Comput. 19(1), 31\u2013100 (2006)","journal-title":"High. Order Symb. Comput."},{"key":"20_CR45","unstructured":"Micro NAV autopilot software. Available http:\/\/sourceforge.net\/projects\/micronav\/"},{"key":"20_CR46","doi-asserted-by":"crossref","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: CC, pp. 213\u2013228 (2002)","DOI":"10.1007\/3-540-45937-5_16"},{"key":"20_CR47","unstructured":"Paparazzi autopilot software. Available http:\/\/wiki.paparazziuav.org\/wiki\/Main_Page"},{"key":"20_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-49727-7_15","volume-title":"Static Analysis","author":"JC Peralta","year":"1998","unstructured":"Peralta, J.C., Gallagher, J.P., Saglam, H.: Analysis of imperative programs through analysis of constraint logic programs. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 246\u2013261. Springer, Heidelberg (1998)"},{"key":"20_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1007\/978-3-319-08867-9_7","volume-title":"Computer Aided Verification","author":"Z Rakamari\u0107","year":"2014","unstructured":"Rakamari\u0107, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 106\u2013113. Springer, Heidelberg (2014)"},{"key":"20_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-642-39799-8_24","volume-title":"Computer Aided Verification","author":"P R\u00fcmmer","year":"2013","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 347\u2013363. Springer, Heidelberg (2013)"},{"key":"20_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"599","DOI":"10.1007\/978-3-642-31424-7_42","volume-title":"Computer Aided Verification","author":"N Sinha","year":"2012","unstructured":"Sinha, N., Singhania, N., Chandra, S., Sridharan, M.: Alternate and learn: finding witnesses without looking all over. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 599\u2013615. Springer, Heidelberg (2012)"},{"key":"20_CR52","doi-asserted-by":"crossref","unstructured":"Steensgaard, B.: Points-to analysis in almost linear time. In: POPL, pp. 32\u201341 (1996)","DOI":"10.1145\/237721.237727"},{"key":"20_CR53","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: LICS, pp. 29\u201337 (2001)","DOI":"10.1109\/LICS.2001.932480"},{"key":"20_CR54","doi-asserted-by":"crossref","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. In: POPL, pp. 427\u2013440 (2012)","DOI":"10.1145\/2103621.2103709"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21690-4_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T06:28:57Z","timestamp":1748500137000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}