December 2013 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Accented letters fixed.
by Roberto Bagnara 28 Dec '13

28 Dec '13

Module: ppl/ppl Branch: master Commit: cabeeaf4154863066f4625802a595a3f812e7acf URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cabeeaf41548… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Dec 28 11:49:13 2013 +0100 Accented letters fixed. --- doc/ppl_citations.bib | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 3798fa2..cdbf314 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -24,7 +24,7 @@ Summarizing: Booktitle = "Static Analysis: Proceedings of the 19th International Symposium (SAS 2012)", Address = "Deauville, France", - Editor = "A. Min{'e} and D. Schmidt", + Editor = "A. Min{\'e} and D. Schmidt", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 7460, @@ -2875,7 +2875,7 @@ Summarizing: Booktitle = "Static Analysis: Proceedings of the 19th International Symposium (SAS 2012)", Address = "Deauville, France", - Editor = "A. Min{'e} and D. Schmidt", + Editor = "A. Min{\'e} and D. Schmidt", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 7460, @@ -2909,7 +2909,7 @@ Summarizing: Booktitle = "Static Analysis: Proceedings of the 19th International Symposium (SAS 2012)", Address = "Deauville, France", - Editor = "A. Min{'e} and D. Schmidt", + Editor = "A. Min{\'e} and D. Schmidt", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 7460,

1 0

[GIT] ppl/ppl(master): More references added.
by Patricia Hill 28 Dec '13

28 Dec '13

Module: ppl/ppl Branch: master Commit: d86bf4a6f5e1353f04d4de18ab0197fda617ad5b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d86bf4a6f5e1… Author: Patricia Hill <patricia.hill(a)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." } +@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." } -@Inproceedings{MihailaSS13a, +@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." } +@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,

1 0

[GIT] ppl/ppl(master): Author field fixed.
by Roberto Bagnara 28 Dec '13

28 Dec '13

Module: ppl/ppl Branch: master Commit: 9580dfe6324b3bc6dddf9cfde3f4668e9858fea4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9580dfe6324b… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Dec 28 09:59:32 2013 +0100 Author field fixed. --- doc/ppl_citations.bib | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 27eab07..573ba03 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -4197,7 +4197,7 @@ Summarizing: } @Inproceedings{SharmaGHAN13, - Author = "R. Sharma and S. Gupta and B. Hariharan and A. Aiken and AV. Nori", + Author = "R. Sharma and S. Gupta and B. Hariharan and A. Aiken and A. V. Nori", Title = "Verification as Learning Geometric Concepts", Booktitle = "Static Analysis: Proceedings of the 20th International Symposium (SAS 2013)",

1 0

[GIT] ppl/ppl(master): Book title fixed.
by Roberto Bagnara 28 Dec '13

28 Dec '13

Module: ppl/ppl Branch: master Commit: 01fd0ad80bf20c095f6a3b03efdb093a4668c138 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=01fd0ad80bf2… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Dec 28 09:57:46 2013 +0100 Book title fixed. --- doc/ppl_citations.bib | 3 ++- 1 files changed, 2 insertions(+), 1 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 5a3dbdd..27eab07 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -4845,7 +4845,8 @@ Summarizing: @Incollection{ZuffereyWH12, Author = "D. Zufferey and T. Wies and T. A. Henzinger", Title = "Ideal Abstractions for Well-Structured Transition Systems", - Booktitle = "Proceedings of 13th International Conference on Verification, Model Checking, and Abstract Interpretation, {VMCAI} 2012", + Booktitle = "Verification, Model Checking, and Abstract Interpretation: + Proceedings of 13th International Conference (VMCAI 2012)", Series = "Lecture Notes in Computer Science", Editor = "V. Kuncak and A. Rybalchenko", Publisher = "Springer-Verlag, Berlin",

1 0

[GIT] ppl/ppl(master): Added missing acronym.
by Roberto Bagnara 28 Dec '13

28 Dec '13

Module: ppl/ppl Branch: master Commit: c8809ae0cddab276e04aabcd7a0f870720e5a691 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c8809ae0cdda… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Dec 28 09:56:13 2013 +0100 Added missing acronym. --- doc/ppl_citations.bib | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index b82f57b..5a3dbdd 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -22,7 +22,7 @@ Summarizing: Author = "A. Albarghouthi and A. Gurfinkel and M. Chechik", Title = "Craig Interpretation", Booktitle = "Static Analysis: - Proceedings of the 19th International Symposium", + Proceedings of the 19th International Symposium (SAS 2012)", Address = "Deauville, France", Editor = "A. Min{'e} and D. Schmidt", Publisher = "Springer-Verlag, Berlin",

1 0

[GIT] ppl/ppl(master): Duplicate key avoided.
by Roberto Bagnara 28 Dec '13

28 Dec '13

Module: ppl/ppl Branch: master Commit: a2462d7deec1083c3cd018b5824eb9c86738b981 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a2462d7deec1… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Dec 28 09:53:29 2013 +0100 Duplicate key avoided. --- doc/ppl_citations.bib | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 2d44d17..b82f57b 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -2127,7 +2127,7 @@ Summarizing: checkers." } -@Inproceedings{MihailaSS13, +@Inproceedings{MihailaSS13a, Author = "P.-L. Garoche and T. Kahsai and C. Tinelli", Title = "Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers", Booktitle = "NASA Formal Methods: @@ -3474,7 +3474,7 @@ Summarizing: } -@Inproceedings{MihailaSS13, +@Inproceedings{MihailaSS13b, Author = "B. Mihaila and A. Sepp and A. Simon", Title = "Widening as Abstract Domain", Booktitle = "NASA Formal Methods:

1 0

[GIT] ppl/ppl(master): Added missing acronym.
by Roberto Bagnara 28 Dec '13

28 Dec '13

Module: ppl/ppl Branch: master Commit: e296eb896b6de97708300660cb3ebf0d93c2419f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e296eb896b6d… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Dec 28 09:52:16 2013 +0100 Added missing acronym. --- doc/ppl_citations.bib | 8 ++++---- 1 files changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 0d36b29..2d44d17 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -470,7 +470,7 @@ Summarizing: Author = "G. Amato and F. Scozzari", Title = "Localizing Widening and Narrowing", Booktitle = "Static Analysis: - Proceedings of the 20th International Symposium", + Proceedings of the 20th International Symposium (SAS 2013)", Address = "Seattle, USA", Series = "Lecture Notes in Computer Science", Editor = "F. Logozzo and M. F{\"a}hndrich", @@ -1808,7 +1808,7 @@ Summarizing: Title = "Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra", Booktitle = "Static Analysis: - Proceedings of the 20th International Symposium", + Proceedings of the 20th International Symposium (SAS 2013)", Address = "Seattle, USA", Series = "Lecture Notes in Computer Science", Editor = "F. Logozzo and M. F{\"a}hndrich", @@ -3625,7 +3625,7 @@ Summarizing: Author = "N. Partush and E. Yahav", Title = "Abstract Semantic Differencing for Numerical Programs", Booktitle = "Static Analysis: - Proceedings of the 20th International Symposium", + Proceedings of the 20th International Symposium (SAS 2013)", Address = "Seattle, WA, USA", Editor = "F. Logozzo and M. F{\"a}hndrich", Publisher = "Springer-Verlag, Berlin", @@ -4200,7 +4200,7 @@ Summarizing: Author = "R. Sharma and S. Gupta and B. Hariharan and A. Aiken and AV. Nori", Title = "Verification as Learning Geometric Concepts", Booktitle = "Static Analysis: - Proceedings of the 20th International Symposium", + Proceedings of the 20th International Symposium (SAS 2013)", Address = "Seattle, USA", Series = "Lecture Notes in Computer Science", Editor = "F. Logozzo and M. F{\"a}hndrich",

1 0

[GIT] ppl/ppl(master): Added missing quote.
by Roberto Bagnara 28 Dec '13

28 Dec '13

Module: ppl/ppl Branch: master Commit: 7f06ec32ba1c7adfad33b86d54f7482afcfc8607 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7f06ec32ba1c… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Dec 28 09:51:31 2013 +0100 Added missing quote. --- doc/ppl_citations.bib | 5 +++-- 1 files changed, 3 insertions(+), 2 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 576c8a2..0d36b29 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -1804,8 +1804,9 @@ Summarizing: } @Inproceedings{FouiheMP13, - Author = "A. Fouilhe and D. Monniaux and M. P{\'e}rin, - Title = "Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra", + Author = "A. Fouilhe and D. Monniaux and M. P{\'e}rin", + Title = "Efficient Generation of Correctness Certificates + for the Abstract Domain of Polyhedra", Booktitle = "Static Analysis: Proceedings of the 20th International Symposium", Address = "Seattle, USA",

1 0

[GIT] ppl/ppl(master): Braces restored.
by Roberto Bagnara 28 Dec '13

28 Dec '13

Module: ppl/ppl Branch: master Commit: d54fe90f1b5346477848a6aef21e7021720c67cf URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d54fe90f1b53… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Dec 28 09:50:51 2013 +0100 Braces restored. --- doc/ppl_citations.bib | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 8a7baab..576c8a2 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -1777,7 +1777,7 @@ Summarizing: Month = jul, Year = 2005, Note = "In German", - Abstract = "Diese Arbeit beschreibt eine intra- und auch + Abstract = "{Diese Arbeit beschreibt eine intra- und auch interprozedurale Datenflussanalyse, welche an jedem Programmpunkt statisch die Beziehungen, die zwischen den Programmvariablen gelten, bestimmen k\"onnen. Die @@ -1800,7 +1800,7 @@ Summarizing: der linearen Algebra die affinen Beziehungen, welche zwischen den Programmvariablen an einem bestimmten Programmpunkt gelten, erkennen. Die Behandlung von - Prozeduraufrufen steht dabei im Vordergrund." + Prozeduraufrufen steht dabei im Vordergrund.}" } @Inproceedings{FouiheMP13,

1 0

[GIT] ppl/ppl(master): Book title corrected.
by Roberto Bagnara 28 Dec '13

28 Dec '13

Module: ppl/ppl Branch: master Commit: dd62f522295c254dc0135f745b2e6202fafcd6f5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=dd62f522295c… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Dec 28 09:49:06 2013 +0100 Book title corrected. --- doc/ppl_citations.bib | 6 ++++-- 1 files changed, 4 insertions(+), 2 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index ca66833..8a7baab 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -2129,7 +2129,8 @@ Summarizing: @Inproceedings{MihailaSS13, Author = "P.-L. Garoche and T. Kahsai and C. Tinelli", Title = "Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers", - Booktitle = "Proceedings of the 5th International Symposium on {NASA} Formal Methods, {NFM} 2013", + Booktitle = "NASA Formal Methods: + Proceedings of the 5th International Symposium (NFM 2013)", Editor = "G. Brat and N. Rungta and A. Venet", Address = "Moffett Field, CA, USA", Pages = "139--154", @@ -3475,7 +3476,8 @@ Summarizing: @Inproceedings{MihailaSS13, Author = "B. Mihaila and A. Sepp and A. Simon", Title = "Widening as Abstract Domain", - Booktitle = "Proceedings of the 5th International Symposium on {NASA} Formal Methods, {NFM} 2013", + Booktitle = "NASA Formal Methods: + Proceedings of the 5th International Symposium (NFM 2013)", Editor = "G. Brat and N. Rungta and A. Venet", Address = "Moffett Field, CA, USA", Pages = "170--174",

1 0