Relational Analysis and Precision via Probabilistic Abstract Interpretation |
| |
Authors: | Alessandra Di Pierro Pascal Sotin Herbert Wiklicky |
| |
Affiliation: | Available online 16 December 2008. |
| |
Abstract: | Within the context of a quantitative generalisation of the well established framework of Abstract Interpretation – i.e. Probabilistic Abstract Interpretation – we investigate a quantitative notion of precision which allows us to compare analyses on the basis of their expected exactness for a given program. We illustrate this approach by considering various types of numerical abstractions of the values of variables for independent analysis as well as weakly and fully relational analysis. We utilise for this a linear operator semantics of a simple imperative programming language. In this setting, fully relational dependencies are realised via the tensor product. Independent analyses and weakly relational analyses are realised as abstractions of the fully relational analysis. |
| |
Keywords: | Probabilistic Semantics Linear Operators Probabilistic Abstract Interpretation Relational Analysis |
本文献已被 ScienceDirect 等数据库收录! |