{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T14:09:41Z","timestamp":1746194981099,"version":"3.37.3"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2018,10,18]],"date-time":"2018-10-18T00:00:00Z","timestamp":1539820800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,10,18]],"date-time":"2018-10-18T00:00:00Z","timestamp":1539820800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"A gift from Rajiv and Ritu Batra"},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-14-2-0270","FA8750-15-C-0082"],"award-info":[{"award-number":["FA8750-14-2-0270","FA8750-15-C-0082"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"name":"UW-Madison Office of the Vice Chancellor for Research and Graduate Education with funding from the Wisconsin Alumni Research Foundation"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2019,8]]},"DOI":"10.1007\/s10703-018-0325-z","type":"journal-article","created":{"date-parts":[[2018,10,18]],"date-time":"2018-10-18T07:07:21Z","timestamp":1539846441000},"page":"110-143","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A new abstraction framework for affine transformers"],"prefix":"10.1007","volume":"54","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5250-9533","authenticated-orcid":false,"given":"Tushar","family":"Sharma","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,18]]},"reference":[{"key":"325_CR1","doi-asserted-by":"crossref","unstructured":"Chen L, Min\u00e9 A, Wang J, Cousot P (2009) Interval polyhedra: an abstract domain to infer interval linear relationships. In: SAS","DOI":"10.1007\/978-3-642-03237-0_21"},{"key":"325_CR2","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1976) Static determination of dynamic properties of programs. In: Proceedings of the 2nd international symposium on programming, Paris","DOI":"10.1145\/390018.808314"},{"key":"325_CR3","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"325_CR4","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1979) Systematic design of program analysis frameworks. In: POPL","DOI":"10.1145\/567752.567778"},{"key":"325_CR5","doi-asserted-by":"crossref","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear constraints among variables of a program. In: POPL","DOI":"10.1145\/512760.512770"},{"key":"325_CR6","doi-asserted-by":"crossref","unstructured":"Elder M, Lim J, Sharma T, Andersen T, Reps T (2014) Abstract domains of affine relations. In: TOPLAS","DOI":"10.1145\/2651361"},{"key":"325_CR7","doi-asserted-by":"crossref","unstructured":"Gange G, Navas J, Schachte P, S\u00f8ndergaard H, Stuckey P (2013) Abstract interpretation over non-lattice abstract domains. In: SAS","DOI":"10.1007\/978-3-642-38856-9_3"},{"key":"325_CR8","doi-asserted-by":"crossref","unstructured":"Goubault E, Putot S, V\u00e9drine F (2012) Modular static analysis with zonotopes. In: CAV","DOI":"10.1007\/978-3-642-33125-1_5"},{"key":"325_CR9","doi-asserted-by":"crossref","unstructured":"Jeannet B, Gopan D, Reps T (2005) A relational abstraction for functions. In: SAS","DOI":"10.1007\/11547662_14"},{"key":"325_CR10","doi-asserted-by":"crossref","unstructured":"Jones N, Mycroft A (1986) Data flow analysis of applicative programs using minimal function graphs. In: POPL, pp 296\u2013306","DOI":"10.1145\/512644.512672"},{"key":"325_CR11","unstructured":"Kidd N, Lal A, Reps T (2007) WALi: the weighted automaton library. www.cs.wisc.edu\/wpis\/wpds\/download.php"},{"key":"325_CR12","doi-asserted-by":"crossref","unstructured":"King A, S\u00f8ndergaard H (2010) Automatic abstraction for congruences. In: VMCAI","DOI":"10.1007\/978-3-642-11319-2_16"},{"key":"325_CR13","doi-asserted-by":"crossref","unstructured":"Knoop J, Steffen B (1992) The interprocedural coincidence theorem. In: CC","DOI":"10.1007\/3-540-55984-1_13"},{"key":"325_CR14","doi-asserted-by":"crossref","unstructured":"Lal A, Reps T, Balakrishnan G (2005) Extended weighted pushdown systems. In: CAV","DOI":"10.1007\/11513988_44"},{"key":"325_CR15","unstructured":"Lattner C, Adve V (2004) LLVM: a compilation framework for lifelong program analysis and transformation. In: International symposium on code generation and optimization"},{"key":"325_CR16","unstructured":"Lim J, Reps T (2008) A system for generating static analyzers for machine instructions. In: CC"},{"issue":"1","key":"325_CR17","doi-asserted-by":"publisher","first-page":"841","DOI":"10.1145\/2450136.2450139","volume":"35","author":"J Lim","year":"2013","unstructured":"Lim J, Reps T (2013) TSL: a system for generating abstract interpreters and its application to machine-code analysis. TOPLAS 35(1):841\u2013847","journal-title":"TOPLAS"},{"key":"325_CR18","unstructured":"LLVM: Low level virtual machine. Llvm.org"},{"key":"325_CR19","unstructured":"Malmkj\u00e6r K (1993) Abstract interpretation of partial-evaluation algorithms. PhD thesis, Department of Computing and Information Sciences, Kansas State University, Manhattan"},{"key":"325_CR20","unstructured":"Min\u00e9 A (2001) The octagon abstract domain. In: WCRE"},{"key":"325_CR21","doi-asserted-by":"crossref","unstructured":"Min\u00e9 A (2002) A few graph-based relational numerical abstract domains. In: SAS","DOI":"10.1007\/3-540-45789-5_11"},{"key":"325_CR22","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm M, Seidl H (2004) Precise interprocedural analysis through linear algebra. In: POPL","DOI":"10.1145\/964001.964029"},{"issue":"5","key":"325_CR23","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1145\/1275497.1275504","volume":"29","author":"M M\u00fcller-Olm","year":"2007","unstructured":"M\u00fcller-Olm M, Seidl H (2007) Analysis of modular arithmetic. TOPLAS 29(5):29","journal-title":"TOPLAS"},{"key":"325_CR24","doi-asserted-by":"crossref","unstructured":"Mycroft A, Jones N (1986) A relational framework for abstract interpretation. In: Programs as data objects. Springer, Berlin, Heidelberg. https:\/\/link.springer.com\/chapter\/10.1007\/3-540-16446-4_9","DOI":"10.1007\/3-540-16446-4_9"},{"key":"325_CR25","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0304-3975(89)90091-1","volume":"69","author":"F Nielson","year":"1989","unstructured":"Nielson F (1989) Two-level semantics and abstract interpretation. Theor Comput Sci 69:117\u2013242","journal-title":"Theor Comput Sci"},{"key":"325_CR26","doi-asserted-by":"crossref","unstructured":"Reps T, Balakrishnan G, Lim J (2006) Intermediate-representation recovery from low-level code. In: Partial evaluation and semantics-based program manipulation","DOI":"10.1145\/1111542.1111560"},{"key":"325_CR27","doi-asserted-by":"crossref","unstructured":"Reps T, Sagiv M, Yorsh G (2004) Symbolic implementation of the best transformer. In: VMCAI","DOI":"10.1007\/978-3-540-24622-0_21"},{"issue":"1\u20132","key":"325_CR28","first-page":"206","volume":"58","author":"T Reps","year":"2005","unstructured":"Reps T, Schwoon S, Jha S, Melski D (2005) Weighted pushdown systems and their application to interprocedural dataflow analysis. SCP 58(1\u20132):206\u2013263","journal-title":"SCP"},{"key":"325_CR29","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan S, Sipma H, Manna Z (2005) Scalable analysis of linear systems using mathematical programming. In: VMCAI","DOI":"10.1007\/978-3-540-30579-8_2"},{"key":"325_CR30","volume-title":"Denotational semantics","author":"D Schmidt","year":"1986","unstructured":"Schmidt D (1986) Denotational semantics. Allyn and Bacon Inc., Boston"},{"key":"325_CR31","doi-asserted-by":"crossref","unstructured":"Sen R, Srikant Y (2007) Executable analysis using abstract interpretation with circular linear progressions. In: MEMOCODE","DOI":"10.1109\/MEMCOD.2007.371251"},{"key":"325_CR32","unstructured":"Sharir M, Pnueli A (1981) Two approaches to interprocedural data flow analysis. In: Muchnick SS, Jones ND (eds) Program flow analysis: theory and applications. Prentice-Hall, Englewood Cliffs, NJ"},{"key":"325_CR33","doi-asserted-by":"crossref","unstructured":"Sharma T, Reps T (2017) Sound bit-precise numerical domains. In: VMCAI","DOI":"10.1007\/978-3-319-52234-0_27"},{"key":"325_CR34","unstructured":"Simon A, King A (2007) Taming the wrapping of integer arithmetic. In: SAS"},{"key":"325_CR35","doi-asserted-by":"crossref","unstructured":"Thakur A, Elder M, Reps T (2012) Bilateral algorithms for symbolic abstraction. In: SAS","DOI":"10.1007\/978-3-642-33125-1_10"},{"key":"325_CR36","volume-title":"Hacker\u2019s delight","author":"H Warren Jr","year":"2003","unstructured":"Warren H Jr (2003) Hacker\u2019s delight. Addison-Wesley, Reading"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-0325-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-018-0325-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-0325-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,4]],"date-time":"2022-09-04T05:27:27Z","timestamp":1662269247000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-018-0325-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,18]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,8]]}},"alternative-id":["325"],"URL":"https:\/\/doi.org\/10.1007\/s10703-018-0325-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2018,10,18]]},"assertion":[{"value":"18 October 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}