{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T03:17:32Z","timestamp":1774063052543,"version":"3.50.1"},"publisher-location":"Cham","reference-count":38,"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_42","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T02:08:27Z","timestamp":1436926107000},"page":"622-640","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":72,"title":["Boosting k-Induction with Continuously-Refined Invariants"],"prefix":"10.1007","author":[{"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[]},{"given":"Matthias","family":"Dangl","sequence":"additional","affiliation":[]},{"given":"Philipp","family":"Wendler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"42_CR1","volume-title":"Compilers: Principles, Techniques, and Tools","author":"AV Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading (1986)"},{"key":"42_CR2","doi-asserted-by":"crossref","unstructured":"Awedh, M., Somenzi, F.: Automatic invariant strengthening to prove properties in bounded model checking. In: Proceedings of DAC, pp. 1073\u20131076. ACM\/IEEE (2006)","DOI":"10.1109\/DAC.2006.229399"},{"key":"42_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: technology transfer of formal methods inside microsoft. In: Proceedings of IFM, LNCS, vol. 2999, pp. 1\u201320. Springer (2004)","DOI":"10.1007\/978-3-540-24756-2_1"},{"issue":"7","key":"42_CR4","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. Commun. ACM 54(7), 68\u201376 (2011)","journal-title":"Commun. ACM"},{"key":"42_CR5","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Proceedings of PASTE, pp. 82\u201387. ACM (2005)","DOI":"10.1145\/1108768.1108813"},{"key":"42_CR6","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Second competition on software verification. In: Proceedings of TACAS, LNCS, vol. 7795, pp. 594\u2013609. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_43"},{"key":"42_CR7","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Software verification and verifiable witnesses. In: Proceedings of TACAS, LNCS, vol. 9035, pp. 401\u2013416. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_31"},{"key":"42_CR8","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Combining k-induction with continuously-refined invariants. Technical Report MIP-1503, University of Passau, January 2015. \n                      arXiv:1502.00096","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"42_CR9","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Proceedings of VMCAI, LNCS, vol. 4349, pp. 378\u2013394. Springer (2007)","DOI":"10.1007\/978-3-540-69738-1_27"},{"key":"42_CR10","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Procedings of PLDI, pp. 300\u2013309. ACM (2007)","DOI":"10.1145\/1273442.1250769"},{"key":"42_CR11","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: Proceedings of ASE, pp. 29\u201338. IEEE (2008)","DOI":"10.1109\/ASE.2008.13"},{"key":"42_CR12","doi-asserted-by":"crossref","unstructured":"Beyer, D., Keremoglu, M.:CPAchecker: A tool for configurable software verification. In: Proceedings of CAV, LNCS, vol. 6806, pp. 184\u2013190. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"42_CR13","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proceedings of FMCAD, pp. 189\u2013197. FMCAD (2010)"},{"key":"42_CR14","doi-asserted-by":"crossref","unstructured":"Beyer, D., L\u00f6we, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Proceedings of FASE, LNCS, vol. 7793, pp. 146\u2013162. Springer (2013)","DOI":"10.1007\/978-3-642-37057-1_11"},{"key":"42_CR15","volume-title":"Handbook of Satisfiability","author":"A Biere","year":"2009","unstructured":"Biere, A.: Handbook of Satisfiability. IOS Press, Amsterdam (2009)"},{"key":"42_CR16","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"key":"42_CR17","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of TACAS, LNCS, vol. 1579, pp. 193\u2013207. Springer (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"issue":"1","key":"42_CR18","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N  Bj\u00f8rner","year":"1997","unstructured":"Bj\u00f8rner, N., Browne, A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theor. Comput. Sci. 173(1), 49\u201387 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"42_CR19","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proceedings of PLDI, pp. 196\u2013207. ACM (2003)","DOI":"10.1145\/780822.781153"},{"issue":"4\u20135","key":"42_CR20","first-page":"379","volume":"20","author":"AR Bradley","year":"2008","unstructured":"Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. FAC 20(4\u20135), 379\u2013405 (2008)","journal-title":"FAC"},{"key":"42_CR21","doi-asserted-by":"crossref","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: An interpolating SMT solver. In: Proceedings of SPIN, LNCS, vol. 7385, pp. 248\u2013254. Springer (2012)","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"42_CR22","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B., Silva, J.P.M.: SMT-based bounded model checking for embedded ANSI-C software. In: Proceedings of ASE, pp. 137\u2013148. IEEE (2009)","DOI":"10.1109\/ASE.2009.63"},{"key":"42_CR23","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Procedings of POPL, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"42_CR24","doi-asserted-by":"crossref","unstructured":"Donaldson, A.F., Haller, L., Kroening, D.: Strengthening induction-based race checking with lightweight static analysis. In: Proceedings of VMCAI, LNCS, vol. 6538, pp. 169\u2013183. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-18275-4_13"},{"key":"42_CR25","doi-asserted-by":"crossref","unstructured":"Donaldson, A.F., Haller, L., Kroening, D., R\u00fcmmer, P.: Software verification using k-induction. In: Proceeding of Static Analysis. LNCS, vol. 6887, pp. 351\u2013368. Springer (2011)","DOI":"10.1007\/978-3-642-23702-7_26"},{"key":"42_CR26","doi-asserted-by":"crossref","unstructured":"Donaldson, A.F., Kroening, D., R\u00fcmmer, P.: Automatic analysis of scratch-pad memory code for heterogeneous multicore processors. In: Proceedings of TACAS, LNCS, vol. 6015, pp. 280\u2013295. Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_24"},{"issue":"1","key":"42_CR27","first-page":"83","volume":"39","author":"AF Donaldson","year":"2011","unstructured":"Donaldson, A.F., Kr\u00f6ning, D., R\u00fcmmer, P.: Automatic analysis of DMA races using model checking and k-induction. FMSD 39(1), 83\u2013113 (2011)","journal-title":"FMSD"},{"key":"42_CR28","doi-asserted-by":"crossref","unstructured":"Garoche, P.-L., Kahsai, T., Tinelli, C.: Incremental invariant generation using logic-based automatic abstract transformers. In: Proceedings of NFM, LNCS, vol. 7871, pp. 139\u2013154. Springer (2013)","DOI":"10.1007\/978-3-642-38088-4_10"},{"key":"42_CR29","doi-asserted-by":"crossref","unstructured":"Gro\u00dfe, D., Le, H.M., Drechsler, R.: Proving transaction and system-level properties of untimed SystemC TLM designs. In: Proceedings of MEMOCODE, pp. 113\u2013122. IEEE (2010)","DOI":"10.1109\/MEMCOD.2010.5558643"},{"key":"42_CR30","doi-asserted-by":"crossref","unstructured":"Gupta, A., Rybalchenko, A.: InvGen: an efficient invariant generator. In: Proceedings of CAV, LNCS, vol. 5643, pp. 634\u2013640. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"42_CR31","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., Gurfinkel, A., Li, Y., Chaki, S., Chechik, M.: UFO: verification with interpolants and abstract interpretation. In: Proceedings of TACAS, LNCS, vol. 7795, pp. 637\u2013640. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_52"},{"key":"42_CR32","doi-asserted-by":"crossref","unstructured":"Kahsai, T., Ge, Y., Tinelli, C.: Instantiation-based invariant discovery. In: Proceedings of NFM, LNCS, vol. 6617, pp. 192\u2013206. Springer (2011)","DOI":"10.1007\/978-3-642-20398-5_15"},{"key":"42_CR33","doi-asserted-by":"crossref","unstructured":"Kahsai, T., Tinelli, C.: Pkind: a parallel k-induction based model checker. In: Proceedings of International Workshop on Parallel and Distributed Methods in Verification, EPTCS 72, pp. 55\u201362 (2011)","DOI":"10.4204\/EPTCS.72.6"},{"key":"42_CR34","doi-asserted-by":"crossref","unstructured":"Khoroshilov, A., Mutilin, V., Petrenko, A., Zakharov, V.: Establishing linux driver verification process. In: Proceedings of PSI, LNCS, vol. 5947, pp. 165\u2013176. Springer (2010)","DOI":"10.1007\/978-3-642-11486-1_14"},{"key":"42_CR35","doi-asserted-by":"crossref","unstructured":"Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Handling unbounded loops with ESBMC 1.20. In: Proceedings of TACAS, LNCS, vol. 7795, pp. 619\u2013622. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_47"},{"key":"42_CR36","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Proceedings of VMCAI, LNCS, vol. 3385, pp. 25\u201341. Springer (2005)","DOI":"10.1007\/978-3-540-30579-8_2"},{"key":"42_CR37","doi-asserted-by":"crossref","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Proceedings of FMCAD, LNCS, vol. 1954, pp. 108\u2013125. Springer (2000)","DOI":"10.1007\/3-540-40922-X_8"},{"key":"42_CR38","unstructured":"Wahl, T.: The k-induction principle (2013). \n                      http:\/\/www.ccs.neu.edu\/home\/wahl\/Publications\/k-induction.pdf"}],"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_42","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T20:11:49Z","timestamp":1563826309000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_42","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"}}]}}