{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:48:29Z","timestamp":1775868509414,"version":"3.50.1"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,9,30]],"date-time":"2012-09-30T00:00:00Z","timestamp":1348963200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We consider the problem of computing numerical invariants of programs, for\ninstance bounds on the values of numerical program variables. More\nspecifically, we study the problem of performing static analysis by abstract\ninterpretation using template linear constraint domains. Such invariants can be\nobtained by Kleene iterations that are, in order to guarantee termination,\naccelerated by widening operators. In many cases, however, applying this form\nof extrapolation leads to invariants that are weaker than the strongest\ninductive invariant that can be expressed within the abstract domain in use.\nAnother well-known source of imprecision of traditional abstract interpretation\ntechniques stems from their use of join operators at merge nodes in the control\nflow graph. The mentioned weaknesses may prevent these methods from proving\nsafety properties. The technique we develop in this article addresses both of\nthese issues: contrary to Kleene iterations accelerated by widening operators,\nit is guaranteed to yield the strongest inductive invariant that can be\nexpressed within the template linear constraint domain in use. It also eschews\njoin operators by distinguishing all paths of loop-free code segments. Formally\nspeaking, our technique computes the least fixpoint within a given template\nlinear constraint domain of a transition relation that is succinctly expressed\nas an existentially quantified linear real arithmetic formula. In contrast to\npreviously published techniques that rely on quantifier elimination, our\nalgorithm is proved to have optimal complexity: we prove that the decision\nproblem associated with our fixpoint problem is in the second level of the\npolynomial-time hierarchy.<\/jats:p>","DOI":"10.2168\/lmcs-8(3:29)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T08:17:46Z","timestamp":1385713066000},"source":"Crossref","is-referenced-by-count":9,"title":["Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs"],"prefix":"10.46298","volume":"Volume 8, Issue 3","author":[{"given":"Thomas Martin","family":"Gawlitza","sequence":"first","affiliation":[]},{"given":"David","family":"Monniaux","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,9,30]]},"reference":[{"key":"687:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/689\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/689\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:54:15Z","timestamp":1681242855000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/689"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,9,30]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(3:29)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1209.0643","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1209.0643","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"arxiv","id":"1709.04382","asserted-by":"subject"},{"id-type":"doi","id":"10.1007\/s00236-018-0324-y","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arxiv.1709.04382","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,9,30]]},"article-number":"689"}}