{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T08:02:43Z","timestamp":1780300963737,"version":"3.54.0"},"reference-count":17,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T00:00:00Z","timestamp":1777507200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2026,8]]},"DOI":"10.1016\/j.scico.2026.103497","type":"journal-article","created":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T14:59:40Z","timestamp":1777647580000},"page":"103497","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Accelerated bounded model checking with LoAT"],"prefix":"10.1016","volume":"253","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0902-1994","authenticated-orcid":false,"given":"Florian","family":"Frohn","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0283-8520","authenticated-orcid":false,"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.scico.2026.103497_bib0001","series-title":"FM \u201824","first-page":"73","article-title":"Integrating loop acceleration into bounded model checking","author":"Frohn","year":"2024"},{"key":"10.1016\/j.scico.2026.103497_bib0002","series-title":"IJCAR \u201822","first-page":"712","article-title":"Proving non-termination and lower runtime bounds with LoAT (System description)","author":"Frohn","year":"2022"},{"key":"10.1016\/j.scico.2026.103497_bib0003","doi-asserted-by":"crossref","unstructured":"F. Frohn, J. Giesl, Integrating Loop Acceleration into Bounded Model Checking (Version 1), 2024. https:\/\/doi.org\/10.5281\/zenodo.11954017.","DOI":"10.1007\/978-3-031-71162-6_4"},{"key":"10.1016\/j.scico.2026.103497_bib0004","series-title":"TACAS \u201825","first-page":"205","article-title":"AProVE(KoAT+LoAT) - (Competition contribution)","author":"Lommen","year":"2025"},{"key":"10.1016\/j.scico.2026.103497_bib0005","unstructured":"C. Barrett, P. Fontaine, C. Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB), 2016. https:\/\/smt-lib.org\/."},{"key":"10.1016\/j.scico.2026.103497_bib0006","series-title":"SAS \u201823","first-page":"259","article-title":"ADCL: acceleration driven clause learning for constrained Horn clauses","author":"Frohn","year":"2023"},{"key":"10.1016\/j.scico.2026.103497_bib0007","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","article-title":"Bounded model checking","volume":"58","author":"Biere","year":"2003","journal-title":"Adv. Comput."},{"key":"10.1016\/j.scico.2026.103497_bib0008","series-title":"FMCAD \u201800","first-page":"108","article-title":"Checking safety properties using induction and a SAT-solver","author":"Sheeran","year":"2000"},{"key":"10.1016\/j.scico.2026.103497_bib0009","series-title":"CADE \u201825","first-page":"468","article-title":"Infinite state model checking by learning transitive relations","author":"Frohn","year":"2025"},{"key":"10.1016\/j.scico.2026.103497_bib0010","series-title":"CADE \u201823","first-page":"220","article-title":"Proving non-termination by acceleration driven clause learning","author":"Frohn","year":"2023"},{"key":"10.1016\/j.scico.2026.103497_bib0011","series-title":"TACAS \u201820","first-page":"58","article-title":"A calculus for modular loop acceleration","author":"Frohn","year":"2020"},{"key":"10.1016\/j.scico.2026.103497_bib0012","series-title":"TACAS \u201822","first-page":"415","article-title":"CVC5: a versatile and industrial-Strength SMT solver","author":"Barbosa","year":"2022"},{"key":"10.1016\/j.scico.2026.103497_bib0013","series-title":"IJCAR \u201824","first-page":"344","article-title":"Satisfiability modulo exponential integer arithmetic","author":"Frohn","year":"2024"},{"key":"10.1016\/j.scico.2026.103497_bib0014","series-title":"CAV \u201814","first-page":"737","article-title":"Yices 2.2","author":"Dutertre","year":"2014"},{"key":"10.1016\/j.scico.2026.103497_bib0015","series-title":"TACAS \u201808","first-page":"337","article-title":"Z3: an efficient SMT solver","author":"de Moura","year":"2008"},{"issue":"5","key":"10.1016\/j.scico.2026.103497_bib0016","doi-asserted-by":"crossref","first-page":"691","DOI":"10.1007\/s10009-022-00670-2","article-title":"A calculus for modular loop acceleration and non-termination proofs","volume":"24","author":"Frohn","year":"2022","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10.1016\/j.scico.2026.103497_bib0017","unstructured":"F. Frohn, J. Giesl, LoATWebsite. https:\/\/loat-developers.github.io\/LoAT\/."}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642326000638?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642326000638?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T07:25:12Z","timestamp":1780298712000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642326000638"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,8]]},"references-count":17,"alternative-id":["S0167642326000638"],"URL":"https:\/\/doi.org\/10.1016\/j.scico.2026.103497","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2026,8]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Accelerated bounded model checking with LoAT","name":"articletitle","label":"Article Title"},{"value":"Science of Computer Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.scico.2026.103497","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 The Author(s). Published by Elsevier B.V.","name":"copyright","label":"Copyright"}],"article-number":"103497"}}