This paper addresses the problem of abstracting a set of affine transformers (Formula presented.), where (Formula presented.) and (Formula presented.) represent the pre-state and post-state, respectively. We introduce a framework to harness any base abstract domain B in an abstract domain of affine transformations. Abstract domains are usually used to define constraints on the variables of a program. In this paper, however, abstract domain B is re-purposed to constrain the elements of C and (Formula presented.) —thereby defining a set of affine transformers on program states. This framework facilitates intra- and interprocedural analyses to obtain function and loop summaries, as well as to prove program assertions.
CITATION STYLE
Sharma, T., & Reps, T. (2017). A new abstraction framework for affine transformers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10422 LNCS, pp. 342–363). Springer Verlag. https://doi.org/10.1007/978-3-319-66706-5_17
Mendeley helps you to discover research relevant for your work.