{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T14:22:06Z","timestamp":1743085326415,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319681665"},{"type":"electronic","value":"9783319681672"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-68167-2_12","type":"book-chapter","created":{"date-parts":[[2017,9,25]],"date-time":"2017-09-25T23:50:53Z","timestamp":1506383453000},"page":"164-183","source":"Crossref","is-referenced-by-count":1,"title":["Compositional Safety Refutation Techniques"],"prefix":"10.1007","author":[{"given":"Kumar","family":"Madhukar","sequence":"first","affiliation":[]},{"given":"Peter","family":"Schrammel","sequence":"additional","affiliation":[]},{"given":"Mandayam","family":"Srivas","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"12_CR1","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). doi:\n10.1007\/978-3-642-27940-9_4"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-48320-9_8","volume-title":"CONCUR\u201999 Concurrency Theory","author":"R Alur","year":"1999","unstructured":"Alur, R., de Alfaro, L., Henzinger, T.A., Mang, F.Y.C.: Automating modular verification. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 82\u201397. Springer, Heidelberg (1999). doi:\n10.1007\/3-540-48320-9_8"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-662-48288-9_9","volume-title":"Static Analysis","author":"M Brain","year":"2015","unstructured":"Brain, M., Joshi, S., Kroening, D., Schrammel, P.: Safety verification and refutation by k-invariants and k-induction. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 145\u2013161. Springer, Heidelberg (2015). doi:\n10.1007\/978-3-662-48288-9_9"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-28891-3_7","volume-title":"NASA Formal Methods","author":"J Brauer","year":"2012","unstructured":"Brauer, J., Simon, A.: Inferring definite counterexamples through under-approximation. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 54\u201369. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-28891-3_7"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Chen, H., David, C., Kroening, D., Schrammel, P., Wachter, B.: Synthesising interprocedural bit-precise termination proofs. In: Automated Software Engineering, pp. 53\u201364. ACM (2015)","DOI":"10.1109\/ASE.2015.10"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). doi:\n10.1007\/10722167_15"},{"issue":"5","key":"12_CR7","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. Trans. Programm. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"Trans. Programm. Lang. Syst."},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: Logic in Computer Science, pp. 353\u2013362. IEEE Computer Society (1989)","DOI":"10.1109\/LICS.1989.39190"},{"key":"12_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. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). doi:\n10.1007\/978-3-540-24730-2_15"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-70545-1_32","volume-title":"Computer Aided Verification","author":"B Cook","year":"2008","unstructured":"Cook, B., Gulwani, S., Lev-Ami, T., Rybalchenko, A., Sagiv, M.: Proving conditional termination. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 328\u2013340. Springer, Heidelberg (2008). doi:\n10.1007\/978-3-540-70545-1_32"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-319-48989-6_12","volume-title":"FM 2016: Formal Methods","author":"C David","year":"2016","unstructured":"David, C., Kesseli, P., Kroening, D., Lewis, M.: Danger invariants. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 182\u2013198. Springer, Cham (2016). doi:\n10.1007\/978-3-319-48989-6_12"},{"key":"12_CR12","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, pp. 234\u2013245. ACM (2002)","DOI":"10.1145\/512529.512558"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Compositional dynamic test generation. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, pp. 47\u201354. ACM, New York (2007)","DOI":"10.1145\/1190216.1190226"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-23702-7_12","volume-title":"Static Analysis","author":"P Godefroid","year":"2011","unstructured":"Godefroid, P., Lahiri, S.K., Rubio-Gonz\u00e1lez, C.: Statically validating must summaries for incremental compositional dynamic test generation. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 112\u2013128. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-23702-7_12"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Programming Language Design and Implementation, pp. 281\u2013292. ACM (2008)","DOI":"10.1145\/1375581.1375616"},{"issue":"3","key":"12_CR16","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1002\/swf.41","volume":"2","author":"M Harman","year":"2001","unstructured":"Harman, M., Hierons, R.M.: An overview of program slicing. Softw. Focus 2(3), 85\u201392 (2001)","journal-title":"Softw. Focus"},{"key":"12_CR17","first-page":"797","volume":"8559","author":"M Heizmann","year":"2014","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Termination analysis by learning terminating programs. Comput.-Aided Verification 8559, 797\u2013813 (2014)","journal-title":"Comput.-Aided Verification"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Bj\u00f8rner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using horn clauses over integers and arrays. In: Formal Methods in Computer-Aided Design, pp. 89\u201396 (2015)","DOI":"10.1109\/FMCAD.2015.7542257"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-17511-4_20"},{"key":"12_CR20","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.entcs.2012.09.009","volume":"287","author":"A Min\u00e9","year":"2012","unstructured":"Min\u00e9, A.: Inferring sufficient conditions with backward polyhedral under-approximations. Electr. Notes Theor. Comput. Sci. 287, 89\u2013100 (2012)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"3","key":"12_CR21","doi-asserted-by":"publisher","first-page":"16:1","DOI":"10.1145\/1740582.1740584","volume":"11","author":"KS Namjoshi","year":"2010","unstructured":"Namjoshi, K.S., Trefler, R.J.: On the completeness of compositional reasoning methods. ACM Trans. Comput. Log. 11(3), 16:1\u201316:22 (2010). doi:\n10.1145\/1740582.1740584","journal-title":"ACM Trans. Comput. Log."},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/11823230_2","volume-title":"Static Analysis","author":"S Sankaranarayanan","year":"2006","unstructured":"Sankaranarayanan, S., Ivan\u010di\u0107, F., Shlyakhter, I., Gupta, A.: Static analysis in disjunctive numerical domains. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 3\u201317. Springer, Heidelberg (2006). doi:\n10.1007\/11823230_2"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Schrammel, P.: Challenges in decomposing encodings of verification problems. In: Horn Clauses for Verification and Synthesis, EPTCS (2016). p. to appear","DOI":"10.4204\/EPTCS.219.3"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"905","DOI":"10.1007\/978-3-662-49674-9_56","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Schrammel","year":"2016","unstructured":"Schrammel, P., Kroening, D.: 2LS for program analysis. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 905\u2013907. Springer, Heidelberg (2016). doi:\n10.1007\/978-3-662-49674-9_56"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-319-19458-5_5","volume-title":"Formal Methods for Industrial Critical Systems","author":"P Schrammel","year":"2015","unstructured":"Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T., Bienm\u00fcller, T.: Successful use of incremental BMC in the automotive industry. In: N\u00fa\u00f1ez, M., G\u00fcdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 62\u201377. Springer, Cham (2015). doi:\n10.1007\/978-3-319-19458-5_5"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-642-34188-5_15","volume-title":"Hardware and Software: Verification and Testing","author":"O Sery","year":"2012","unstructured":"Sery, O., Fedyukovich, G., Sharygina, N.: Interpolation-based function summaries in bounded model checking. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 160\u2013175. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-34188-5_15"},{"key":"12_CR27","unstructured":"SPARK: (2014). \nhttp:\/\/www.spark-2014.org\/"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68167-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,10,3]],"date-time":"2017-10-03T03:51:18Z","timestamp":1507002678000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68167-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319681665","9783319681672"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68167-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}