{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:02Z","timestamp":1747592462894},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2015,4,17]],"date-time":"2015-04-17T00:00:00Z","timestamp":1429228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2015,8]]},"DOI":"10.1007\/s10703-015-0228-1","type":"journal-article","created":{"date-parts":[[2015,4,16]],"date-time":"2015-04-16T10:58:31Z","timestamp":1429181911000},"page":"75-92","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Under-approximating loops in C programs for fast counterexample detection"],"prefix":"10.1007","volume":"47","author":[{"given":"Daniel","family":"Kroening","sequence":"first","affiliation":[]},{"given":"Matt","family":"Lewis","sequence":"additional","affiliation":[]},{"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,17]]},"reference":[{"key":"228_CR1","doi-asserted-by":"crossref","unstructured":"Ball T, Cook B, Levin V, Rajamani SK (2004) Slam and static driver verifier: technology transfer of formal methods inside Microsoft. In: IFM, LNCS, vol 2999. Springer, New York","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"228_CR2","unstructured":"Beyer D (2014) Status report on software verification\u2014(competition summary SV-COMP 2014). In: TACAS, LNCS, vol 8413. Springer, New York, pp 373\u2013388"},{"key":"228_CR3","doi-asserted-by":"crossref","unstructured":"Beyer D, Henzinger TA, Majumdar R, Rybalchenko A (2007) Path invariants. In: PLDI. ACM, pp 300\u2013309","DOI":"10.1145\/1250734.1250769"},{"key":"228_CR4","unstructured":"Boigelot B (1999) Symbolic methods for exploring infinite state spaces. Ph.D. thesis, Universit\u00e9 de Li\u00e8ge"},{"key":"228_CR5","doi-asserted-by":"crossref","unstructured":"Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: TACAS. Springer, New York, pp 168\u2013176","DOI":"10.1007\/978-3-540-24730-2_15"},{"issue":"5","key":"228_CR6","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1145\/1941487.1941509","volume":"54","author":"B Cook","year":"2011","unstructured":"Cook B, Podelski A, Rybalchenko A (2011) Proving program termination. Commun ACM 54(5):88\u201398","journal-title":"Commun ACM"},{"key":"228_CR7","doi-asserted-by":"crossref","unstructured":"van Engelen R, Birch J, Gallivan K (2004) Array data dependence testing with the chains of recurrences algebra. In: IEEE Innovative architecture for future generation high-performance processors and systems, pp 70\u201381","DOI":"10.1109\/IWIA.2004.10018"},{"key":"228_CR8","doi-asserted-by":"crossref","unstructured":"Finkel A, Leroux J (2002) How to compose Presburger-accelerations: applications to broadcast protocols. In: FST-TCS 2002, LNCS, vol 2556. Springer, New York, pp 145\u2013156","DOI":"10.1007\/3-540-36206-1_14"},{"key":"228_CR9","doi-asserted-by":"crossref","unstructured":"Handjieva M, Tzolovski S (1998) Refining static analyses by trace-based partitioning using control flow. In: SAS, LNCS, vol 1503. Springer, New York, pp 200\u2013214","DOI":"10.1007\/3-540-49727-7_12"},{"key":"228_CR10","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: POPL. ACM, pp 58\u201370","DOI":"10.1145\/503272.503279"},{"key":"228_CR11","doi-asserted-by":"crossref","unstructured":"Hojjat H, Iosif R, Konecny F, Kuncak V, Ruemmer P (2012) Accelerating interpolants. In: ATVA, LNCS. Springer, New York 7561:197\u2013202","DOI":"10.1007\/978-3-642-33386-6_16"},{"key":"228_CR12","doi-asserted-by":"crossref","unstructured":"Jhala R, McMillan KL (2006) A practical and complete approach to predicate refinement. In: TACAS, LNCS, vol 3920. Springer, New York, pp 459\u2013473","DOI":"10.1007\/11691372_33"},{"key":"228_CR13","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs L, Voronkov A (2009) Finding loop invariants for programs over arrays using a theorem prover. In: FASE, LNCS, vol 5503. Springer, New York, pp 470\u2013485","DOI":"10.1109\/SYNASC.2009.66"},{"key":"228_CR14","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs LI, Jebelean T (2005) An algorithm for automated generation of invariants for loops with conditionals. In: IEEE symposium on symbolic and numeric algorithms for scientific computing (SYNASC), pp 245\u2013249","DOI":"10.1109\/SYNASC.2005.19"},{"key":"228_CR15","doi-asserted-by":"crossref","unstructured":"Kroening D, Sharygina N, Tonetta S, Tsitovich A, Wintersteiger CM (2008) Loop summarization using abstract transformers. In: ATVA, LNCS, vol 5311. Springer, New York, pp 111\u2013125","DOI":"10.1007\/978-3-540-88387-6_10"},{"key":"228_CR16","doi-asserted-by":"crossref","unstructured":"Kroening D, Weissenbacher G (2006) Counterexamples with loops for predicate abstraction. In: CAV, LNCS, vol 4144. Springer, New York, pp 152\u2013165","DOI":"10.1007\/11817963_16"},{"key":"228_CR17","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/s00165-009-0110-2","volume":"22","author":"D Kroening","year":"2010","unstructured":"Kroening D, Weissenbacher G (2010) Verification and falsification of programs with loops using predicate abstraction. Form Asp Comput 22:105\u2013128","journal-title":"Form Asp Comput"},{"key":"228_CR18","doi-asserted-by":"crossref","unstructured":"Ku K, Hart TE, Chechik M, Lie D (2007) A buffer overflow benchmark for software model checkers. In: ASE. ACM, pp 389\u2013392. doi: 10.1145\/1321631.1321691","DOI":"10.1145\/1321631.1321691"},{"key":"228_CR19","doi-asserted-by":"crossref","unstructured":"McMillan KL (2006) Lazy abstraction with interpolants. In: CAV, LNCS, vol 4144. Springer, New York, pp 123\u2013136","DOI":"10.1007\/11817963_14"},{"issue":"4","key":"228_CR20","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1145\/69558.69559","volume":"11","author":"G Nelson","year":"1989","unstructured":"Nelson G (1989) A generalization of Dijkstra\u2019s calculus. TOPLAS 11(4):517\u2013561","journal-title":"TOPLAS"},{"key":"228_CR21","doi-asserted-by":"crossref","unstructured":"Sharma R, Dillig I, Dillig T, Aiken A (2011) Simplifying loop invariant generation using splitter predicates. In: CAV, LNCS, vol 6806. Springer, New York, pp 703\u2013719","DOI":"10.1007\/978-3-642-22110-1_57"},{"key":"228_CR22","doi-asserted-by":"crossref","unstructured":"Sinha N (2008) Symbolic program analysis using term rewriting and generalization. In: Formal methods in computer-aided design, pp 1\u20139","DOI":"10.1109\/FMCAD.2008.ECP.23"},{"key":"228_CR23","volume-title":"Supercompilers for parallel and vector computers","author":"H Zima","year":"1991","unstructured":"Zima H, Chapman B (1991) Supercompilers for parallel and vector computers. ACM, New York"},{"key":"228_CR24","doi-asserted-by":"crossref","unstructured":"Zuleger F, Gulwani S, Sinn M, Veith H (2011) Bound analysis of imperative programs with the size-change abstraction. In: SAS, LNCS, vol 6887. Springer, New York, pp 280\u2013297","DOI":"10.1007\/978-3-642-23702-7_22"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0228-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-015-0228-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0228-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,26]],"date-time":"2019-03-26T22:53:22Z","timestamp":1553640802000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-015-0228-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,4,17]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["228"],"URL":"https:\/\/doi.org\/10.1007\/s10703-015-0228-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,4,17]]}}}