December 2013 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Fixed bogus label.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: 0d00cfeb5cc6eccd934ef864e4f45731374995ee URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0d00cfeb5cc6… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 10:57:17 2013 +0100 Fixed bogus label. --- 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 26eb69d..9ef85bc 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -3458,7 +3458,7 @@ Summarizing: \url{http://www.irisa.fr/manifestations/2006/CSTVA06/}." } -@Inproceedings{L, +@Inproceedings{LegayT13, Author = "A. Legay and L.-M. Traonouez", Title = "{PyEcdar}: Towards Open Source Implementation for Timed Systems", Booktitle = "Automated Technology for Verification and Analysis:

1 0

[GIT] ppl/ppl(master): Several corrections.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: 5cee161f40429e641ad64c2630055221ab896633 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5cee161f4042… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 10:53:57 2013 +0100 Several corrections. --- doc/ppl_citations.bib | 14 ++++++++------ 1 files changed, 8 insertions(+), 6 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index e185442..26eb69d 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -577,8 +577,8 @@ Summarizing: Title = "Merge and Conquer: State Merging in Parametric Timed Automata", Booktitle = "Automated Technology for Verification and Analysis: Proceedings of the 11th International Symposium (ATVA 2013)", - Editor = "D. {Van Hung} and M. Ogawa", Address = "Hanoi, Vietnam", + Editor = "D. {Van Hung} and M. Ogawa", Pages = "381--396", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", @@ -1044,7 +1044,7 @@ Summarizing: } @InProceedings{BozgaIK12, - Author = "M. Bozga and R. Iosif and F. Kone\v{c}n\'y", + Author = "M. Bozga and R. Iosif and F. Kone\v{c}n\'{y}", Title = "Deciding Conditional Termination", Booktitle = "Tools and Algorithms for the Construction and Analysis of Systems: Proceedings of the 18th International Conference @@ -1155,12 +1155,14 @@ Summarizing: } @Inproceedings{BrihayeDGQRW13, - Author = "T. Brihaye and L. Doyen and G. Geeraerts and J. Ouaknine and J.-F. Raskin and J. Worrell", - Title = "Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points", + Author = "T. Brihaye and L. Doyen and G. Geeraerts and J. Ouaknine + and J.-F. Raskin and J. Worrell", + Title = "Time-Bounded Reachability for Monotonic Hybrid Automata: + Complexity and Fixed Points", Booktitle = "Automated Technology for Verification and Analysis: Proceedings of the 11th International Symposium (ATVA 2013)", Address = "Hanoi, Vietnam", - Editor = "Dang {Van Hung}", + Editor = "D. {Van Hung} and M. Ogawa", Year = 2013, Pages = "55--70", Publisher = "Springer-Verlag, Berlin", @@ -3460,7 +3462,7 @@ Summarizing: Author = "A. Legay and L.-M. Traonouez", Title = "{PyEcdar}: Towards Open Source Implementation for Timed Systems", Booktitle = "Automated Technology for Verification and Analysis: - proceedings of the 11th International Symposium, {ATVA} 2013", + Proceedings of the 11th International Symposium (ATVA 2013)", Address = "Hanoi, Vietnam", Editor = "D. {Van Hung} and M. Ogawa", Pages = "460--463",

1 0

[GIT] ppl/ppl(master): More corrections.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: b39bc85755ec2fbc5c740c59052193f1fc02ecf1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b39bc85755ec… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 10:38:17 2013 +0100 More corrections. --- doc/ppl_citations.bib | 11 ++++++----- 1 files changed, 6 insertions(+), 5 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 6d686e9..e185442 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -3077,7 +3077,7 @@ Summarizing: @Article{Jakubczy12k, Author = "K. Jakubczyk", Title = "Sweeping in Abstract Interpretation", - Journal = "Electronic Notes in Theoretical Computer Science ({ENTCS})", + Journal = "Electronic Notes in Theoretical Computer Science", Publisher = "Elsevier Science Publishers B. V.", Address = "Amsterdam, The Netherlands", Volume = 288, @@ -3187,7 +3187,7 @@ Summarizing: Author = "D. Kapur and Z. Zhang and M. Horbach and H. Zhao and Q. Lu and T. Nguyen", Title = "Geometric Quantifier Elimination Heuristics - for Automatically Generating Octagonal and Max-plus Invariants", + for Automatically Generating Octagonal and Max-Plus Invariants", Booktitle = "Automated Reasoning and Mathematics: Essays in Memory of William W. McCune", Editor = "M. P. Bonacina and M. E. Stickel", @@ -3571,8 +3571,9 @@ Summarizing: } @article{LuMMRFL12, - Author = "Q. Lu and M. Madsen and M. Milata and S. Ravn and U. Fahrenberg and K. G. Larsen", - Title = "Reachability analysis for timed automata using max-plus algebra", + Author = "Q. Lu and M. Madsen and M. Milata and S. Ravn and U. Fahrenberg + and K. G. Larsen", + Title = "Reachability Analysis for Timed Automata using Max-Plus Algebra", ISSN = "1567-8326", Journal = "Journal of Logic and Algebraic Programming", Volume = 81, @@ -3587,7 +3588,7 @@ Summarizing: backward reachability analysis using max-plus polyhedra. To show that the approach works in practice and theory alike, we have created a proof-of-concept - implementation on top of the model checker opaal." + implementation on top of the model checker \texttt{opaal}." } @Inproceedings{MakhloufK06,

1 0

[GIT] ppl/ppl(master): Several corrections.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: 8fb99a8c84bb175cc116f98215d600a11d2efc25 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8fb99a8c84bb… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 10:33:00 2013 +0100 Several corrections. --- doc/ppl.bib | 5 +++-- doc/ppl_citations.bib | 40 ++++++++++++++++++++-------------------- 2 files changed, 23 insertions(+), 22 deletions(-) diff --git a/doc/ppl.bib b/doc/ppl.bib index cbb16bb..931706e 100644 --- a/doc/ppl.bib +++ b/doc/ppl.bib @@ -1670,8 +1670,9 @@ Summarizing: @InProceedings{GopanDMDRS04, Author = "D. Gopan and F. DiMaio and N. Dor and T. W. Reps and M. Sagiv", Title = "Numeric Domains with Summarized Dimensions", - Booktitle = "Tools and Algorithms for the Construction and Analysis - of Systems, 10th International Conference, TACAS 2004", + Booktitle = "Proceedings of the 10th International Conference + Tools and Algorithms for the Construction and Analysis + of Systems (TACAS 2004)", Address = "Barcelona, Spain", Editor = "K. Jensen and A. Podelski", Publisher = "Springer-Verlag, Berlin", diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index da581a2..6d686e9 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -665,9 +665,9 @@ Summarizing: @Inproceedings{ArmandoBM07, Author = "A. Armando and M. Benerecetti and J. Mantovani", Title = "Abstraction Refinement of Linear Programs with Arrays", - Booktitle = "Proceedings of the 13th International Conference on - Tools and Algorithms for the Construction and Analysis - of Systems (TACAS 2007)", + Booktitle = "Tools and Algorithms for the Construction and Analysis + of Systems: Proceedings of the 13th International Conference + (TACAS 2007)", Address = "Braga, Portugal", Editor = "O. Grumberg and M. Huth", Publisher = "Springer-Verlag, Berlin", @@ -1008,9 +1008,9 @@ Summarizing: @Inproceedings{BozgaGI09, Author = "M. Bozga and C. G\^{\i}rlea and R. Iosif", Title = "Iterating Octagons", - Booktitle = "Proceedings of the 15th International Conference on - Tools and Algorithms for the Construction and Analysis - of Systems (TACAS 2009)", + Booktitle = "Tools and Algorithms for the Construction and Analysis + of Systems: Proceedings of the 15th International Conference + (TACAS 2009)", Address = "York, UK", Editor = "S. Kowalewski and A. Philippou", Publisher = "Springer-Verlag, Berlin", @@ -1047,8 +1047,8 @@ Summarizing: Author = "M. Bozga and R. Iosif and F. Kone\v{c}n\'y", Title = "Deciding Conditional Termination", Booktitle = "Tools and Algorithms for the Construction and Analysis - of Systems: - 18th International Conference, {TACAS} 2012", + of Systems: Proceedings of the 18th International Conference + (TACAS 2012)", Address = "Tallinn, Estonia", Editor = "C. Flanagan and B. K{\"o}nig", Publisher = "Springer-Verlag, Berlin", @@ -2328,7 +2328,7 @@ Summarizing: 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)", + Proceedings of the 13th International Conference (VMCAI 2012)", Address = "Philadelphia, PA, USA", Editor = "V. Kuncak and A. Rybalchenko", Publisher = "Springer-Verlag, Berlin", @@ -2781,9 +2781,9 @@ Summarizing: @Inproceedings{GulavaniR06, Author = "B. S. Gulavani and S. K. Rajamani", Title = "Counterexample Driven Refinement for Abstract Interpretation", - Booktitle = "Proceedings of the 12th International Conference on - Tools and Algorithms for the Construction and Analysis - of Systems (TACAS 2006)", + Booktitle = "Tools and Algorithms for the Construction and Analysis + of Systems: Proceedings of the 12th International Conference + (TACAS 2006)", Address = "Vienna, Austria", Editor = "H. Hermanns and J. Palsberg", Pages = "474--488", @@ -3089,11 +3089,11 @@ Summarizing: adapted for static analysis of computer software by abstract interpretation. We expose how concept of the sweeping line can be used to represent elements of a - numerical abstract domain of boxes, which is a + numerical abstract domain of \emph{boxes}, which is a disjunctive refinement of a well known domain of - intervals that allows finite number of disjunctions. We - provide a detailed description of the representation - along with standard domain operations + \emph{intervals} that allows finite number of + disjunctions. We provide a detailed description of the + representation along with standard domain operations algorithms. Furthermore we introduce very precise widening operator for the domain. Additionally we show that the presented idea of the representation based on @@ -3479,9 +3479,9 @@ Summarizing: Author = "D. Lime and O. H. Roux and C. Seidner and L.-M. Traonouez", Title = "Romeo: A Parametric Model-Checker for {Petri} Nets with Stopwatches", - Booktitle = "Proceedings of the 15th International Conference - Tools and Algorithms for the Construction and Analysis - of Systems (TACAS 2009)", + Booktitle = "Tools and Algorithms for the Construction and Analysis + of Systems: Proceedings of the 15th International Conference + (TACAS 2009)", Address = "York, UK", Editor = "S. Kowalewski and A. Philippou", Publisher = "Springer-Verlag, Berlin", @@ -3795,7 +3795,7 @@ Summarizing: } -@Inproceedings{MihailaSS13b, +@Inproceedings{MihailaSS13, Author = "B. Mihaila and A. Sepp and A. Simon", Title = "Widening as Abstract Domain", Booktitle = "NASA Formal Methods:

1 0

[GIT] ppl/ppl(master): Fixed CostantiniFM13.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: 6fcac6790f7a0fef514b652eec08a2850dd6715e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6fcac6790f7a… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 10:22:02 2013 +0100 Fixed CostantiniFM13. --- 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 f5b7ac2..da581a2 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -1469,11 +1469,11 @@ Summarizing: } @Inproceedings{CostantiniFM13, - author = "G. Costantini and P. Ferrara and G. Maggiore", - title = "The Domain of Parametric Hypercubes for Static Analysis of Computer Games Software", + 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", + Proceedings of 15th International Conference (ICFEM 2013)", Address = "Queenstown, New Zealand", Series = "Lecture Notes in Computer Science", Editor = "L. Groves and J. Sun",

1 0

[GIT] ppl/ppl(master): Fixed BrauerKK13.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: 1a892e8f245a03c131bcda659b67528b3dd74817 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1a892e8f245a… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 10:18:35 2013 +0100 Fixed BrauerKK13. --- doc/ppl_citations.bib | 7 ++++--- 1 files changed, 4 insertions(+), 3 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 1c0c7fa..f5b7ac2 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -1128,12 +1128,13 @@ Summarizing: @Article{BrauerKK13, Author = "J. Brauer and A King. and S. Kowalewski", - Title = "Abstract interpretation of microcontroller code: Intervals meet congruences", + Title = "Abstract Interpretation of Microcontroller Code: + Intervals Meet Congruences", Journal = "Science of Computer Programming", Volume = 78, - Number = "7", + Number = 7, Pages = "862--883", - Year = 2006, + Year = 2013, Publisher = "Elsevier North-Holland, Inc.", Address = "Amsterdam, The Netherlands", ISSN = "0167-6423",

1 0

[GIT] ppl/ppl(master): Fixed KapurZHZLN13.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: fdcab35567fd8b9031b4dff2e968476485f74ebd URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fdcab35567fd… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 10:12:27 2013 +0100 Fixed KapurZHZLN13. --- doc/ppl_citations.bib | 25 ++++++++++++++----------- 1 files changed, 14 insertions(+), 11 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 1df5397..1c0c7fa 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -3183,8 +3183,10 @@ Summarizing: } @InCollection{KapurZHZLN13, - Author = "D. Kapur and Z. Zhang and M. Horbach and H. Zhao and Q. Lu and T. Nguyen", - Title = "Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants", + Author = "D. Kapur and Z. Zhang and M. Horbach and H. Zhao and Q. Lu + and T. Nguyen", + Title = "Geometric Quantifier Elimination Heuristics + for Automatically Generating Octagonal and Max-plus Invariants", Booktitle = "Automated Reasoning and Mathematics: Essays in Memory of William W. McCune", Editor = "M. P. Bonacina and M. E. Stickel", @@ -3197,26 +3199,27 @@ Summarizing: Abstract = "Geometric heuristics for the quantifier elimination approach presented by Kapur (2004) are investigated to automatically derive loop invariants expressing weakly - relational numerical properties (such as l =< x =< h or - l =< +/- x +/- y =< h) for imperative programs. Such properties + relational numerical properties (such as $l \leq x \leq h$ or + $l \leq \pm x \pm y \leq h)$ for imperative programs. + Such properties have been successfully used to analyze commercial software consisting of hundreds of thousands of lines of code (using for example, the Astr\'ee tool based on abstract interpretation framework proposed by Cousot and his group). The main attraction of the proposed approach is its much lower complexity in contrast to the abstract - interpretation approach (O(n^2) in contrast to O(n^4), - where n is the number of variables) with the ability to + interpretation approach ($O(n^2)$ in contrast to $O(n^4)$, + where $n$ is the number of variables) with the ability to still generate invariants of comparable strength. This approach has been generalized to consider disjunctive invariants of the similar form, expressed using maximum - function (such as max (x + a,y + b,z + c,d) ≤ max - (x + e,y + f,z + g,h)), thus enabling automatic - generation of a subclass of disjunctive invariants for - imperative programs as well." + function (such as + $\max(x + a, y + b, z + c, d) \leq \max (x + e, y + f, z + g, h)$), + thus enabling automatic generation of a subclass of + disjunctive invariants for imperative programs as well." } -@Incollection {KhalilGP09, +@Incollection{KhalilGP09, Author = "G. Khalil and E. Goubault and S. Putot", Title = "The Zonotope Abstract Domain {Taylor1+}", Booktitle = "Computer Aided Verification:

1 0

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

28 Dec '13

Module: ppl/ppl Branch: master Commit: fdfdec5cf566c6693c7b452a571e60b995251317 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fdfdec5cf566… Author: Patricia Hill <patricia.hill(a)bugseng.com> Date: Sat Dec 28 21:42:08 2013 +0000 More references added. --- doc/ppl_citations.bib | 173 ++++++++++++++++++++++++++++++++++++++++++------- 1 files changed, 149 insertions(+), 24 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=fdfdec5c…

1 0

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

28 Dec '13

Module: ppl/ppl Branch: master Commit: 22e8ceb3a871bcc8dff3c7fabd14e611ece9598a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=22e8ceb3a871… Author: Patricia Hill <patricia.hill(a)bugseng.com> Date: Sat Dec 28 18:13:44 2013 +0000 More references added. --- doc/ppl.bib | 34 -------------- doc/ppl_citations.bib | 115 +++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 115 insertions(+), 34 deletions(-) diff --git a/doc/ppl.bib b/doc/ppl.bib index bc5a897..cbb16bb 100644 --- a/doc/ppl.bib +++ b/doc/ppl.bib @@ -1967,40 +1967,6 @@ Summarizing: Year = 1994, } -@InCollection{KapurZHZLN13, - Author = "D. Kapur and Z. Zhang and M. Horbach and H. Zhao and Q. Lu and T. Nguyen", - Title = "Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants", - Booktitle = "Automated Reasoning and Mathematics: - Essays in Memory of William W. McCune", - Editor = "M. P. Bonacina and M. E. Stickel", - Publisher = "Springer-Verlag, Berlin", - Series = "Lecture Notes in Computer Science", - Volume = 7788, - Pages = "189--228", - Year = 2013, - ISBN = "978-3-642-36674-1 (Print) 978-3-642-36675-8 (Online)" - Abstract = "Geometric heuristics for the quantifier elimination - approach presented by Kapur (2004) are investigated to - automatically derive loop invariants expressing weakly - relational numerical properties (such as l =< x =< h or - l =< +/- x +/- y =< h) for imperative programs. Such properties - have been successfully used to analyze commercial - software consisting of hundreds of thousands of lines of - code (using for example, the Astr\'ee tool based on - abstract interpretation framework proposed by Cousot and - his group). The main attraction of the proposed approach - is its much lower complexity in contrast to the abstract - interpretation approach (O(n^2) in contrast to O(n^4), - where n is the number of variables) with the ability to - still generate invariants of comparable strength. This - approach has been generalized to consider disjunctive - invariants of the similar form, expressed using maximum - function (such as max (x + a,y + b,z + c,d) ≤ max - (x + e,y + f,z + g,h)), thus enabling automatic - generation of a subclass of disjunctive invariants for - imperative programs as well." -} - @Article{KhachiyanBBEG06, Author = "L. Khachiyan and E. Boros and K. Borys and K. Elbassioni and V. Gurvich", diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index e6e4f6f..e412fb8 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -1043,6 +1043,45 @@ Summarizing: number of test cases." } +@InProceedings{BozgaIK12, + Author = "M. Bozga and R. Iosif and F. Kone\vcn\'y", + Title = "Deciding Conditional Termination", + Booktitle = "Tools and Algorithms for the Construction and Analysis + of Systems: + 18th International Conference, {TACAS} 2012", + Address = "Tallinn, Estonia", + Editor = "C. Flanagan and B. K{\"o}nig", + Publisher = "Springer-Verlag, Berlin", + Series = "Lecture Notes in Computer Science", + Volume = 7214, + ISBN = "978-3-642-28755-8 (Print) 978-3-642-28756-5 (Online)", + Pages = "252--266", + Year = 2012, + Abstract = "This paper addresses the problem of conditional + termination, which is that of defining the set of + initial configurations from which a given program + terminates. First we define the dual set, of initial + configurations, from which a non-terminating execution + exists, as the greatest fixpoint of the pre-image of the + transition relation. This definition enables the + representation of this set, whenever the closed form of + the relation of the loop is definable in a logic that + has quantifier elimination. This entails the + decidability of the termination problem for such + loops. Second, we present effective ways to compute the + weakest precondition for non-termination for difference + bounds and octagonal (non-deterministic) relations, by + avoiding complex quantifier eliminations. We also + investigate the existence of linear ranking functions + for such loops. Finally, we study the class of linear + affine relations and give a method of + under-approximating the termination precondition for a + non-trivial subclass of affine relations. We have + performed preliminary experiments on transition systems + modeling real-life systems, and have obtained + encouraging results." +} + @Inproceedings{BramanM08, Title = "Safety Verification of Fault Tolerant Goal-based Control Programs with Estimation Uncertainty", @@ -3090,6 +3129,40 @@ Summarizing: interpretation." } +@InCollection{KapurZHZLN13, + Author = "D. Kapur and Z. Zhang and M. Horbach and H. Zhao and Q. Lu and T. Nguyen", + Title = "Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants", + Booktitle = "Automated Reasoning and Mathematics: + Essays in Memory of William W. McCune", + Editor = "M. P. Bonacina and M. E. Stickel", + Publisher = "Springer-Verlag, Berlin", + Series = "Lecture Notes in Computer Science", + Volume = 7788, + Pages = "189--228", + Year = 2013, + ISBN = "978-3-642-36674-1 (Print) 978-3-642-36675-8 (Online)", + Abstract = "Geometric heuristics for the quantifier elimination + approach presented by Kapur (2004) are investigated to + automatically derive loop invariants expressing weakly + relational numerical properties (such as l =< x =< h or + l =< +/- x +/- y =< h) for imperative programs. Such properties + have been successfully used to analyze commercial + software consisting of hundreds of thousands of lines of + code (using for example, the Astr\'ee tool based on + abstract interpretation framework proposed by Cousot and + his group). The main attraction of the proposed approach + is its much lower complexity in contrast to the abstract + interpretation approach (O(n^2) in contrast to O(n^4), + where n is the number of variables) with the ability to + still generate invariants of comparable strength. This + approach has been generalized to consider disjunctive + invariants of the similar form, expressed using maximum + function (such as max (x + a,y + b,z + c,d) ≤ max + (x + e,y + f,z + g,h)), thus enabling automatic + generation of a subclass of disjunctive invariants for + imperative programs as well." +} + @Incollection {KhalilGP09, Author = "G. Khalil and E. Goubault and S. Putot", Title = "The Zonotope Abstract Domain {Taylor1+}", @@ -3604,6 +3677,28 @@ Summarizing: } +@Article{MonniauxG12, + Author = "D. Monniaux and J. {Le Guen}", + Title = "Stratified Static Analysis Based on Variable Dependencies", + Journal = "Electronic Notes in Theoretical Computer Science ({ENTCS})", + Publisher = "Elsevier Science Publishers B. V.", + Address = "Amsterdam, The Netherlands", + Volume = 288, + Pages = "61--74", + Year = 2012, + ISSN = "1571-0661", + Abstract = "In static analysis by abstract interpretation, one often + uses widening operators in order to enforce convergence + within finite time to an inductive invariant. Certain + widening operators, including the classical one over + finite polyhedra, exhibit an unintuitive behavior: + analyzing the program over a subset of its variables may + lead a more precise result than analyzing the original + program! In this article, we present simple workarounds + for such behavior." + +} + @Inproceedings{MihailaSS13b, Author = "B. Mihaila and A. Sepp and A. Simon", Title = "Widening as Abstract Domain", @@ -4026,6 +4121,26 @@ Summarizing: cost." } +@article{LuMMRFL12, + Author = "Q. Lu and M. Madsen and M. Milata and S. Ravn and U. Fahrenberg and K. G. Larsen", + Title = "Reachability analysis for timed automata using max-plus algebra", + ISSN = "1567-8326", + Journal = "Journal of Logic and Algebraic Programming", + Volume = 81, + Number = 3, + Year = 2012, + Abstract = "We show that max-plus polyhedra are usable as a data + structure in reachability analysis of timed + automata. Drawing inspiration from the extensive work + that has been done on difference bound matrices, as well + as previous work on max-plus polyhedra in other areas, we + develop the algorithms needed to perform forward and + backward reachability analysis using max-plus + polyhedra. To show that the approach works in practice + and theory alike, we have created a proof-of-concept + implementation on top of the model checker opaal." +} + @Article{RizkBFS09, Author = "A. Rizk and G. Batt and F. Fages and S. Soliman", Title = "A General Computational Method for Robustness Analysis

1 0

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

28 Dec '13

Module: ppl/ppl Branch: master Commit: 2f1203b99f97684a6c7b52747fe785595b421940 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2f1203b99f97… Author: Patricia Hill <patricia.hill(a)bugseng.com> Date: Sat Dec 28 13:00:59 2013 +0000 More references added. --- doc/ppl.bib | 34 +++++++++++++++++++++++++++++ doc/ppl_citations.bib | 57 +++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 91 insertions(+), 0 deletions(-) diff --git a/doc/ppl.bib b/doc/ppl.bib index cbb16bb..bc5a897 100644 --- a/doc/ppl.bib +++ b/doc/ppl.bib @@ -1967,6 +1967,40 @@ Summarizing: Year = 1994, } +@InCollection{KapurZHZLN13, + Author = "D. Kapur and Z. Zhang and M. Horbach and H. Zhao and Q. Lu and T. Nguyen", + Title = "Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants", + Booktitle = "Automated Reasoning and Mathematics: + Essays in Memory of William W. McCune", + Editor = "M. P. Bonacina and M. E. Stickel", + Publisher = "Springer-Verlag, Berlin", + Series = "Lecture Notes in Computer Science", + Volume = 7788, + Pages = "189--228", + Year = 2013, + ISBN = "978-3-642-36674-1 (Print) 978-3-642-36675-8 (Online)" + Abstract = "Geometric heuristics for the quantifier elimination + approach presented by Kapur (2004) are investigated to + automatically derive loop invariants expressing weakly + relational numerical properties (such as l =< x =< h or + l =< +/- x +/- y =< h) for imperative programs. Such properties + have been successfully used to analyze commercial + software consisting of hundreds of thousands of lines of + code (using for example, the Astr\'ee tool based on + abstract interpretation framework proposed by Cousot and + his group). The main attraction of the proposed approach + is its much lower complexity in contrast to the abstract + interpretation approach (O(n^2) in contrast to O(n^4), + where n is the number of variables) with the ability to + still generate invariants of comparable strength. This + approach has been generalized to consider disjunctive + invariants of the similar form, expressed using maximum + function (such as max (x + a,y + b,z + c,d) ≤ max + (x + e,y + f,z + g,h)), thus enabling automatic + generation of a subclass of disjunctive invariants for + imperative programs as well." +} + @Article{KhachiyanBBEG06, Author = "L. Khachiyan and E. Boros and K. Borys and K. Elbassioni and V. Gurvich", diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index cdbf314..e6e4f6f 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -1087,6 +1087,33 @@ Summarizing: hypersurfaces) are computed." } +@Article{BrauerKK13, + Author = "J. Brauer and A King. and S. Kowalewski", + Title = "Abstract interpretation of microcontroller code: Intervals meet congruences", + Journal = "Science of Computer Programming", + Volume = 78, + Number = "7", + Pages = "862--883", + Year = 2006, + Publisher = "Elsevier North-Holland, Inc.", + Address = "Amsterdam, The Netherlands", + ISSN = "0167-6423", + Abstract = "Bitwise instructions, loops and indirect data access + present challenges to the verification of + microcontroller programs. In particular, since registers + are often memory mapped, it is necessary to show that an + indirect store operation does not accidentally mutate a + register. To prove this and related properties, this + article advocates using the domain of bitwise linear + congruences in conjunction with intervals to derive + accurate range information. The paper argues that these + two domains complement one another when reasoning about + microcontroller code. The paper also explains how SAT + solving, which applied with dichotomic search, can be + used to recover branching conditions from binary code + which, in turn, further improves interval analysis." +} + @Inproceedings{BrihayeDGQRW13, Author = "T. Brihaye and L. Doyen and G. Geeraerts and J. Ouaknine and J.-F. Raskin and J. Worrell", Title = "Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points", @@ -2954,6 +2981,36 @@ Summarizing: techniques." } +@Article{Jakubczy12k, + Author = "K. Jakubczyk", + Title = "Sweeping in Abstract Interpretation", + Journal = "Electronic Notes in Theoretical Computer Science ({ENTCS})", + Publisher = "Elsevier Science Publishers B. V.", + Address = "Amsterdam, The Netherlands", + Volume = 288, + Pages = "25--36", + Year = 2012, + ISSN = "1571-0661", + Abstract = "In this paper we present how sweeping line techniques, + which are very popular in computational geometry, can be + adapted for static analysis of computer software by + abstract interpretation. We expose how concept of the + sweeping line can be used to represent elements of a + numerical abstract domain of boxes, which is a + disjunctive refinement of a well known domain of + intervals that allows finite number of disjunctions. We + provide a detailed description of the representation + along with standard domain operations + algorithms. Furthermore we introduce very precise + widening operator for the domain. Additionally we show + that the presented idea of the representation based on + sweeping line technique is a generalisation of the + representation that uses Linear Decision Diagrams (LDD), + which is one of possible optimisations of our idea. We + also show that the presented widening operator is often + more precise than the previous one." +} + @Article{JhalaM09, Author = "R. Jhala and R. Majumdar", Title = "Software Model Checking",

1 0