[PPL-devel] [GIT] ppl/ppl(master): Added abstract of Fu13th.

[Roberto Bagnara]

Module: ppl/ppl
Branch: master
Commit: 0032c63a93d8d7ca1330fb796d4c802f9766f1aa
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0032c63a93d8d7ca1330fb796d4c802f9766f1aa

Author: Roberto Bagnara <roberto.bagnara at 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."
 }
 
+ at 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."
 }
 
- at 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: