{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T20:37:37Z","timestamp":1773952657489,"version":"3.50.1"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,9,17]],"date-time":"2012-09-17T00:00:00Z","timestamp":1347840000000},"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>Traditionally, transfer functions have been designed manually for each\noperation in a program, instruction by instruction. In such a setting, a\ntransfer function describes the semantics of a single instruction, detailing\nhow a given abstract input state is mapped to an abstract output state. The net\neffect of a sequence of instructions, a basic block, can then be calculated by\ncomposing the transfer functions of the constituent instructions. However,\nprecision can be improved by applying a single transfer function that captures\nthe semantics of the block as a whole. Since blocks are program-dependent, this\napproach necessitates automation. There has thus been growing interest in\ncomputing transfer functions automatically, most notably using techniques based\non quantifier elimination. Although conceptually elegant, quantifier\nelimination inevitably induces a computational bottleneck, which limits the\napplicability of these methods to small blocks. This paper contributes a method\nfor calculating transfer functions that finesses quantifier elimination\naltogether, and can thus be seen as a response to this problem. The\npracticality of the method is demonstrated by generating transfer functions for\ninput and output states that are described by linear template constraints,\nwhich include intervals and octagons.<\/jats:p>","DOI":"10.2168\/lmcs-8(3:17)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":2,"title":["Transfer Function Synthesis without Quantifier Elimination"],"prefix":"10.46298","volume":"Volume 8, Issue 3","author":[{"given":"J\u00f6rg","family":"Brauer","sequence":"first","affiliation":[]},{"given":"Andy","family":"King","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,9,17]]},"reference":[{"key":"680:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/814\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/814\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:56:36Z","timestamp":1681242996000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/814"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,9,17]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(3:17)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1207.4286","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1207.4286","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,9,17]]},"article-number":"814"}}