{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,13]],"date-time":"2024-02-13T13:03:52Z","timestamp":1707829432874},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"S3","license":[{"start":{"date-parts":[[2018,2,22]],"date-time":"2018-02-22T00:00:00Z","timestamp":1519257600000},"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":["Cluster Comput"],"published-print":{"date-parts":[[2019,5]]},"DOI":"10.1007\/s10586-018-1911-y","type":"journal-article","created":{"date-parts":[[2018,2,22]],"date-time":"2018-02-22T07:16:07Z","timestamp":1519283767000},"page":"6219-6229","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["An improved method of k-induction combined with predicate abstraction and CEGAR for software model checking"],"prefix":"10.1007","volume":"22","author":[{"given":"Shun","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ye","family":"Du","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhen","family":"Han","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,2,22]]},"reference":[{"key":"1911_CR1","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S.: Counterexample-guided abstraction refinement. In: Proceedings of the 12th International Conference on Computer Aided Verification, Chicago, USA, pp. 154\u2013169 (2000)","DOI":"10.1007\/10722167_15"},{"key":"1911_CR2","doi-asserted-by":"crossref","unstructured":"Roohi, N., Prabhakar, P., Viswanathan, M.: Hybridization based CEGAR for hybrid automata with affine dynamics. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, The Netherlands, pp. 752\u2013769 (2016)","DOI":"10.1007\/978-3-662-49674-9_48"},{"key":"1911_CR3","doi-asserted-by":"crossref","unstructured":"Prabhakar, P., Soto, M.G.: Counterexample guided abstraction refinement for stability analysis. In: Proceedings of the 28th International Conference on Computer Aided Verification, Toronto, Canada, pp. 495\u2013512 (2016)","DOI":"10.1007\/978-3-319-41528-4_27"},{"key":"1911_CR4","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-319-39570-8_11","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"\u00c1kos Hajdu","year":"2016","unstructured":"Hajdu, \u00c1., T\u00f3th, T., V\u00f6r\u00f6s, A., et al.: A configurable CEGAR framework with interpolation-based refinements. In: 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems, pp. 158\u2013174. Springer, Heidelberg (2016)"},{"key":"1911_CR5","first-page":"184","volume":"6806","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. Comput. Sci. 6806, 184\u2013190 (2011)","journal-title":"Comput. Sci."},{"key":"1911_CR6","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-54862-8_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Stefan L\u00f6we","year":"2014","unstructured":"L\u00f6we, S., Mandrykin, M., Wendler, P.: CPAchecker, with sequential combination of explicit-value analyses and predicate analyses. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 392\u2013394. Springer, Berlin (2014)"},{"key":"1911_CR7","doi-asserted-by":"crossref","unstructured":"Friedberger, K.: CPA-BAM: block-abstraction memorization with value analysis and predicate analysis. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Netherlands, pp. 912\u2013915 (2016)","DOI":"10.1007\/978-3-662-49674-9_58"},{"key":"1911_CR8","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation, USA, pp. 70\u201387 (2011)","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"1911_CR9","doi-asserted-by":"publisher","first-page":"831","DOI":"10.1007\/978-3-319-08867-9_55","volume-title":"Computer Aided Verification","author":"Johannes Birgmeier","year":"2014","unstructured":"Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Proceedings of the 26th International Conference on Computer Aided Verification, Vienna, Austria, pp. 831\u2013848 (2014)"},{"issue":"3","key":"1911_CR10","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/s10703-016-0257-4","volume":"49","author":"A Cimatti","year":"2016","unstructured":"Cimatti, A., Griggio, A., Mover, S.: Infinite-state invariant checking with IC3 and predicate abstraction. Form. Methods Syst. Des. 49(3), 190\u2013218 (2016)","journal-title":"Form. Methods Syst. Des."},{"key":"1911_CR11","doi-asserted-by":"crossref","unstructured":"G\u00fcnther, H., Laarman, A., Weissenbacher, G.: Vienna verification tool: IC3 for parallel software. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, The Netherlands, pp. 954\u2013957 (2016)","DOI":"10.1007\/978-3-662-49674-9_69"},{"key":"1911_CR12","doi-asserted-by":"crossref","unstructured":"Rocha, W., Rocha, H., Ismail, H.: DepthK: A k-induction verifier based on invariant inference for C programs. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Greece, pp. 360\u2013364 (2017)","DOI":"10.1007\/978-3-662-54580-5_23"},{"key":"1911_CR13","doi-asserted-by":"crossref","unstructured":"Karpenkov, E.G.: LPI: software verification with local policy iteration. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, The Netherlands, pp. 930\u2013933 (2016)","DOI":"10.1007\/978-3-662-49674-9_63"},{"key":"1911_CR14","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Proceedings of the 27th International Conference on Computer Aided Verification, California, USA, pp. 622\u2013640 (2015)","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"1911_CR15","doi-asserted-by":"publisher","first-page":"55","DOI":"10.4204\/EPTCS.72.6","volume":"72","author":"T Kahsai","year":"2011","unstructured":"Kahsai, T., Tinelli, C.: Pkind: a parallel k-induction based model checker. Electronic Proceedings in Theoretical Computer Science 72, 55\u201362 (2011)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"1911_CR16","doi-asserted-by":"crossref","unstructured":"Hickey, R.: The Clojure programming language. In: Proceedings of the 2008 Symposium on Dynamic languages, Cyprus, p. 1 (2008)","DOI":"10.1145\/1408681.1408682"},{"key":"1911_CR17","doi-asserted-by":"crossref","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Proceedings of the 19th International Conference on Model Checking Software, Oxford, UK, pp. 248\u2013254 (2012)","DOI":"10.1007\/978-3-642-31759-0_19"}],"container-title":["Cluster Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10586-018-1911-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-018-1911-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-018-1911-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,4]],"date-time":"2019-11-04T17:58:20Z","timestamp":1572890300000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10586-018-1911-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,2,22]]},"references-count":17,"journal-issue":{"issue":"S3","published-print":{"date-parts":[[2019,5]]}},"alternative-id":["1911"],"URL":"https:\/\/doi.org\/10.1007\/s10586-018-1911-y","relation":{},"ISSN":["1386-7857","1573-7543"],"issn-type":[{"value":"1386-7857","type":"print"},{"value":"1573-7543","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,2,22]]},"assertion":[{"value":"5 December 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 January 2018","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 January 2018","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 February 2018","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}