
handle: 11562/313107
We develop a methodology for constructing semantics-based analyses of programs by approximating their probabilistic semantics. The framework we introduce resembles the one based on Galois connections used in abstract interpretation, the main difference being the choice of linear space structures instead of order-theoretic ones as semantical (concrete and abstract) domains. The intrinsic quantitative nature of linear spaces makes the method suitable for investigations on the problem of a numerical comparison of abstract interpretations with respect to their precision. After introducing the notion of probabilistic abstract interpretation, we define a measure of its precision by means of the norm of a linear operator which encodes the "incompleteness" of the abstraction. Finally we show the application of our results in a series of classical examples.
Closure operators, Abstract Interpretation, Probabilistic programming
Closure operators, Abstract Interpretation, Probabilistic programming
| 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. | Top 10% | |
| 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% |
