[PPL-devel] [GIT] ppl/ppl(master): More references added.

[Patricia Hill]

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

Author: Patricia Hill <patricia.hill at bugseng.com>
Date:   Sat Dec 28 09:42:16 2013 +0000

More references added.

---

 doc/ppl_citations.bib |   77 +++++++++++++++++++++++++++++++++++++++++++++++-
 1 files changed, 75 insertions(+), 2 deletions(-)

diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index 573ba03..3798fa2 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -1401,6 +1401,45 @@ Summarizing:
               implementation over several benchmark systems."
 }
 
+ at Inproceedings{CostantiniFM13,
+  author    = "G. Costantini and P. Ferrara and G. Maggiore",
+  title     = "The Domain of Parametric Hypercubes for Static Analysis of Computer Games Software",
+  Booktitle = "Formal Methods and Software Engineering:
+               Proceedings of 15th International Conference on Formal
+               Engineering Methods, {ICFEM} 2013",
+  Address = "Queenstown, New Zealand",
+  Series = "Lecture Notes in Computer Science",
+  Editor = "L. Groves and J. Sun",
+  Publisher = "Springer-Verlag, Berlin",
+  ISBN = "978-3-642-41201-1 (Print) 978-3-642-41202-8 (Online)",
+  Pages =  "447--463",
+  Volume = 8144,
+  Year = 2013,
+  Abstract = "Computer Games Software deeply relies on physics
+              simulations, which are particularly demanding to analyze
+              because they manipulate a large amount of interleaving
+              floating point variables. Therefore, this application
+              domain is an interesting workbench to stress the
+              trade-off between accuracy and efficiency of abstract
+              domains for static analysis.
+
+              In this paper, we introduce Parametric Hypercubes, a
+              novel disjunctive non-relational abstract domain. Its
+              main features are: (i) it combines the low computational
+              cost of operations on (selected) multidimensional
+              intervals with the accuracy provided by lifting to a
+              power-set disjunctive domain, (ii) the compact
+              representation of its elements allows to limit the space
+              complexity of the analysis, and (iii) the parametric
+              nature of the domain provides a way to tune the
+              accuracy/efficiency of the analysis by just setting the
+              widths of the hypercubes sides.
+
+              The first experimental results on a representative
+              Computer Games case study outline both the efficiency
+              and the precision of the proposal."
+}
+
 @Inproceedings{CovaFBV06,
   Author = "M. Cova and V. Felmetsger and G. Banks and G. Vigna",
   Title = "Static Detection of Vulnerabilities in x86 Executables",
@@ -2127,7 +2166,7 @@ Summarizing:
               checkers."
 }
 
- at Inproceedings{MihailaSS13a,
+ at Inproceedings{GarocheKT13,
   Author = "P.-L. Garoche and T. Kahsai and C. Tinelli",
   Title = "Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers",
   Booktitle = "NASA Formal Methods:
@@ -2164,6 +2203,40 @@ Summarizing:
               our method."
 }
 
+ at Inproceedings{GhorbalIBMG12,
+  Author = "K Ghorbal and F Ivan{\vc}i{\'c} and G Balakrishnan and N Maeda",
+  Title = "Donut Domains:
+           Efficient Non-convex Domains for Abstract Interpretation",
+  Booktitle = "Verification, Model Checking, and Abstract Interpretation:
+               Proceedings of the 13th International Conference ({VMCAI} 2012)",
+  Address = "Philadelphia, PA, USA",
+  Editor = "V. Kuncak and A. Rybalchenko",
+  Publisher = "Springer-Verlag, Berlin",
+  Volume = 7148,
+  Year = 2012,
+  Pages = "235--250",
+  ISBN = "978-3-642-27939-3 (Print) 978-3-642-27940-9 (Online)",
+  Abstract = "Program analysis using abstract interpretation has been
+              successfully applied in practice to find runtime bugs or
+              prove software correct. Most abstract domains that are
+              used widely rely on convexity for their
+              scalability. However, the ability to express non-convex
+              properties is sometimes required in order to achieve a
+              precise analysis of some numerical properties. This work
+              combines already known abstract domains in a novel way
+              in order to design new abstract domains that tackle some
+              non-convex invariants. The abstract objects of interest
+              are encoded as a pair of two convex abstract objects:
+              the first abstract object defines an over-approximation
+              of the possible reached values, as is done
+              customarily. The second abstract object
+              under-approximates the set of impossible values within
+              the state-space of the first abstract object. Therefore,
+              the geometrical concretization of our objects is defined
+              by a convex set minus another convex set (or hole). We
+              thus call these domains donut domains."
+}
+
 @PhdThesis{Gobert07th,
   Author = "F. Gobert",
   Title = "Towards putting abstract interpretation of {Prolog} into practice:
@@ -3599,7 +3672,7 @@ Summarizing:
 @Article{PanizoG12,
   Author = "L. Panizo and M.-d.-M. Gallardo",
   Title = "An extension of Java PathFinder for hybrid systems",
-  Booktitle = "ACM SIGSOFT Software Engineering Notes",
+  Journal = "ACM SIGSOFT Software Engineering Notes",
   Volume = 37,
   Number = 6,
   Year = 2012,