
We propose a method for automatically generating abstract transformers for static analysis by abstract interpretation. The method focuses on linear constraints on programs operating on rational, real or floating-point variables and containing linear assignments and tests. Given the specification of an abstract domain, and a program block, our method automatically outputs an implementation of the corresponding abstract transformer. It is thus a form of program transformation. In addition to loop-free code, the same method also applies for obtaining least fixed points as functions of the precondition, which permits the analysis of loops and recursive functions. The motivation of our work is data-flow synchronous programming languages, used for building control-command embedded systems, but it also applies to imperative and functional programming. Our algorithms are based on quantifier elimination and symbolic manipulation techniques over linear arithmetic formulas. We also give less general results for nonlinear constraints and nonlinear program constructs.
FOS: Computer and information sciences, program transformation, Computer Science - Logic in Computer Science, F.3.1; F.3.2; F.4.1, Logic, linear inequalities, computer science - logic in computer science, abstract interpretation, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], BC1-199, Computer Science - Programming Languages, f.3.1, computer science - programming languages, f.3.2, f.4.1, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], QA75.5-76.95, 004, Logic in Computer Science (cs.LO), quantifier elimination, Electronic computers. Computer science, F.3.2, F.4.1, F.3.1, Programming Languages (cs.PL)
FOS: Computer and information sciences, program transformation, Computer Science - Logic in Computer Science, F.3.1; F.3.2; F.4.1, Logic, linear inequalities, computer science - logic in computer science, abstract interpretation, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], BC1-199, Computer Science - Programming Languages, f.3.1, computer science - programming languages, f.3.2, f.4.1, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], QA75.5-76.95, 004, Logic in Computer Science (cs.LO), quantifier elimination, Electronic computers. Computer science, F.3.2, F.4.1, F.3.1, Programming Languages (cs.PL)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 18 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
