Module: ppl/ppl Branch: master Commit: 0032c63a93d8d7ca1330fb796d4c802f9766f1aa URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0032c63a93d8d...
Author: Roberto Bagnara roberto.bagnara@bugseng.com Date: Sun Dec 29 12:21:25 2013 +0100
Added abstract of Fu13th.
---
doc/ppl_citations.bib | 58 ++++++++++++++++++++++++++++++++++++++---------- 1 files changed, 46 insertions(+), 12 deletions(-)
diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 9c0fa83..deaa40f 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -2233,6 +2233,52 @@ Summarizing: system benchmark from the literature." }
+@PhDThesis{Fu13th, + Title = "Static Analysis of Numerical Properties in the Presence of Pointers", + Author = "Z. Fu", + Type = "Th`{e}se pour le grade de + {``Docteur de l'Universit'e de Rennes 1''}", + School = "'{E}cole doctorale MATISSE, Universit'{e} de Rennes 1 + sous le sceau de l'Universit'e Europ'eenne de Bretagne", + Address = "Rennes, France", + Month = dec, + Year = 2013, + Abstract = "The fast and furious pace of change in computing + technology has become an article of faith for many. The + reliability of computer-based systems cru- cially + depends on the correctness of its computing. Can man, + who created the computer, be capable of preventing + machine-made misfortune? The theory of static analysis + strives to achieve this ambition. The analysis of + numerical properties of programs has been an essential + research topic for static analysis. These kinds of + properties are commonly modeled and handled by the + concept of numerical abstract domains. Unfor- tunately, + lifting these domains to heap-manipulating programs is + not obvious. On the other hand, points-to analyses have + been intensively studied to an- alyze pointer behaviors + and some scale to very large programs but without + inferring any numerical properties. We propose a + framework based on the theory of abstract interpretation + that is able to combine existing numerical domains and + points-to analyses in a modular way. The static + numerical anal- ysis is prototyped using the SOOT + framework for pointer analyses and the PPL library for + numerical domains. The implementation is able to analyze + large Java program within several minutes. The second + part of this thesis consists of a theoretical study of + the com- bination of the points-to analysis with another + pointer analysis providing information called + must-alias. Two pointer variables must alias at some + pro- gram control point if they hold equal reference + whenever the control point is reached. We have developed + an algorithm of quadruple complexity that sharpens + points-to analysis using must-alias information. The + algorithm is proved correct following a semantics-based + formalization and the concept of bisimulation borrowed + from the game theory, model checking etc." +} + @Inproceedings{Fu14a, Author = "Z. Fu", Title = "Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java", @@ -2285,18 +2331,6 @@ Summarizing: scalability." }
-@PhDThesis{Fu13th, - Title = "Static Analysis of Numerical Properties in the Presence of Pointers", - Author = "Z. Fu", - Type = "Th`{e}se pour le grade de - {``Docteur de l'Universit'e de Rennes 1''}", - School = "'{E}cole doctorale MATISSE, Universit'{e} de Rennes 1 - sous le sceau de l'Universit'e Europ'eenne de Bretagne", - Address = "Rennes, France", - Month = dec, - Year = 2013, -} - @Article{GallardoP13, Author = "M.-d.-M. Gallardo and L. Panizo", Title = "Extending Model Checkers for Hybrid System Verification: