×

Relational analysis and precision via probabilistic abstract interpretation. (English) Zbl 1286.68034

Aldini, Alessandro (ed.) et al., Proceedings of the 6th workshop on quantitative aspects of programming languages (QAPL 2008), Budapest, Hungary, March 29–30, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 220, No. 3, 23-42 (2008).
Summary: Within the context of a quantitative generalisation of the well established framework of Interpretation – i.e., probabilistic 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.
For the entire collection see [Zbl 1280.68012].

MSC:

68N15 Theory of programming languages
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ben-Israel, A.; Greville, T. N.E., Generalised Inverses (2003), Springer Verlag
[2] Birkhoff, G.; von Neumann, J., The logic of quantum mechanics, Annals of Mathematics, 37, 823-843 (1936) · JFM 62.1061.04
[3] Böttcher, A.; Silbermann, B., Introduction to Large Truncated Toeplitz Matrices (1999), Springer Verlag · Zbl 0916.15012
[4] Conway, John, A Course in Functional Analysis, Graduate Texts in Mathematics, volume 96 (1990), Springer Verlag · Zbl 0706.46003
[5] Cousot, P.; Cousot, R., Systematic Design of Program Analysis Frameworks, (Proceedings of POPL’79 (1979)), 269-282 · Zbl 0788.68094
[6] Di Pierro, A.; Hankin, C.; Wiklicky, H., Measuring the confinement of probabilistic systems, Theoretical Computer Science, 340, 1, 3-56 (2005) · Zbl 1142.68444
[7] Di Pierro, A.; Hankin, C.; Wiklicky, H., On probabilistic techniques for data flow analysis, Proceedings of QAPL’07. Proceedings of QAPL’07, ENTCS, 190, 59-77 (2007) · Zbl 1279.68034
[8] A. Di Pierro, C. Hankin, and H. Wiklicky. A systematic approach to probabilistic pointer analysis. Proceedings of APLAS’07, to appear; A. Di Pierro, C. Hankin, and H. Wiklicky. A systematic approach to probabilistic pointer analysis. Proceedings of APLAS’07, to appear · Zbl 1137.68352
[9] Di Pierro, A.; Wiklicky, H., Concurrent Constraint Programming: Towards Probabilistic Abstract Interpretation, (Proceedings of PPDP’00 (2000)), 127-138
[10] Di Pierro, A.; Wiklicky, H., Measuring the precision of abstract interpretations, (Proc. of LOPSTR’00. Proc. of LOPSTR’00, LNCS, volume 2042 (2001), Springer Verlag), 147-164 · Zbl 1018.68505
[11] Feller, W., An Introduction to Probability Theory and Its Applications, Vol. 1 (1970), Wiley & Sons: Wiley & Sons New York · Zbl 0158.34902
[12] Jones, N. D.; Muchnick, S. S., Complexity of flow analysis, inductive assertion synthesis and a language due to Dijkstra, (Muchnick, S. S.; Jones, N. D., Program Flow Analysis: Theory and Applications (1981), Prentice-Hall), 380-393
[13] Kadison, R. V.; Ringrose, J. R., Fundamentals of the Theory of Operator Algebras I, Graduate Studies in Mathematics, volume 15 (1997), AMS · Zbl 0888.46039
[14] A. Miné. Weakly Relational Numerical Abstract Domains; A. Miné. Weakly Relational Numerical Abstract Domains
[15] Monier, J. M., Analyse MP (2004), Dunod
[16] Nielson, F.; Riis Nielson, H.; Hankin, C., Principles of Program Analysis (1999), Springer Verlag · Zbl 0932.68013
[17] A. Rountev, S. Kagan, and M. Gibas. Evaluating the imprecision of static analysis. In Workshop on Program Analysis for Software Tools and Engineering; A. Rountev, S. Kagan, and M. Gibas. Evaluating the imprecision of static analysis. In Workshop on Program Analysis for Software Tools and Engineering
[18] Francesca Scozzari. Domain theory in abstract interpretation: equations, completeness and logic; Francesca Scozzari. Domain theory in abstract interpretation: equations, completeness and logic · Zbl 1053.68579
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.