- PPL-devel - BUGSENG Mailman

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

29 Dec '13

Module: ppl/ppl Branch: master Commit: 077dd1051a9af69a1c9599f8e061de1c40f594fe URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=077dd1051a9a… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 12:15:59 2013 +0100 Added Zu14th. --- doc/ppl_citations.bib | 12 ++++++++++++ 1 files changed, 12 insertions(+), 0 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 3bbf21c..9c0fa83 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -2285,6 +2285,18 @@ 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:

1 0

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

29 Dec '13

Module: ppl/ppl Branch: master Commit: 753472710977408c9937bf2951901b330840c13e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=753472710977… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 12:04:28 2013 +0100 Added Fu14b. --- doc/ppl_citations.bib | 29 ++++++++++++++++++++++++++++- 1 files changed, 28 insertions(+), 1 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 4e47958..3bbf21c 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -2233,7 +2233,7 @@ Summarizing: system benchmark from the literature." } -@Inproceedings{Fu14, +@Inproceedings{Fu14a, Author = "Z. Fu", Title = "Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java", Booktitle = "Verification, Model Checking, and Abstract Interpretation: @@ -2242,6 +2242,7 @@ Summarizing: Editor = "K. McMillan and X. Rival", Publisher = "Springer-Verlag, Berlin", Year = 2014, + Note = "To appear", Abstract = "This paper contributes to a new abstract domain that combines static numeric analysis and points-to analysis. One particularity of this abstract domain lies @@ -2258,6 +2259,32 @@ Summarizing: separately." } +@Inproceedings{Fu14b, + Author = "Z. Fu", + Title = "Targeted Update -- Aggressive Memory Abstraction Beyond Common + Sense and its Application on Static Numeric Analysis", + Booktitle = "Proceedings of the 23rd European Symposium on Programming + (ESOP'14)", + Address = "Grenoble, France", + Editor = "Z. Shao", + Publisher = "Springer-Verlag, Berlin", + Year = 2014, + Note = "To appear", + Abstract = "Summarizing techniques are widely used in the reasoning + of unbounded data structures. These techniques prohibit + strong update unless certain restricted safety + conditions are satisfied. We find that by setting and + enforcing the analysis boundaries to a limited scope of + program identifiers, called targets in this paper, more + cases of strong update can be shown sound, not with + regard to the entire heap, but with regard to the + targets. We have implemented the analysis for inferring + numeric properties in Java programs. The experimental + results show a tangible precision enhancement compared + with classical approaches while preserving high + scalability." +} + @Article{GallardoP13, Author = "M.-d.-M. Gallardo and L. Panizo", Title = "Extending Model Checkers for Hybrid System Verification:

1 0

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

29 Dec '13

Module: ppl/ppl Branch: master Commit: 11b8475ea5b751cd65199563d7fd947cf26e10ab URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=11b8475ea5b7… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 11:41:21 2013 +0100 Several improvements. --- doc/ppl.bib | 4 ++-- doc/ppl_citations.bib | 20 ++++++++++++-------- 2 files changed, 14 insertions(+), 10 deletions(-) diff --git a/doc/ppl.bib b/doc/ppl.bib index 931706e..9374746 100644 --- a/doc/ppl.bib +++ b/doc/ppl.bib @@ -744,8 +744,8 @@ Summarizing: and the Double Description Method", Journal = "Formal Aspects of Computing", Publisher = "Springer-Verlag, London", - Volume = "17", - Number = "2", + Volume = 17, + Number = 2, Pages = "222--257", Year = 2005, ISSN = "0934-5043", diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 32e3a39..4e47958 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -1016,7 +1016,7 @@ Summarizing: Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 5505, - Pages = "337-351", + Pages = "337--351", Year = 2009, ISBN = "978-3-642-00767-5", Abstract = "In this paper we prove that the transitive closure of a @@ -1307,7 +1307,7 @@ Summarizing: Booktitle = "Computer Aided Verification: Proceedings of the 25th International Conference (CAV 2013)", Year = 2013, - Pages = "511-526", + Pages = "511--526", Editor = "N. Sharygina and H. Veith", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", @@ -3837,11 +3837,14 @@ Summarizing: merely aim for precision." } -@Inproceedings{MontenegroSEP12, - Author = "M. Montenegro and O. Shkaravska and M. {van Eekelen} and R. Pe\~{n}a", - Title = "Interpolation-Based Height Analysis for Improving a Recurrence Solver", +@Incollection{MontenegroSEP12, + Author = "M. Montenegro and O. Shkaravska and M. {van Eekelen} + and R. Pe\~{n}a", + Title = "Interpolation-Based Height Analysis for Improving + a Recurrence Solver", Booktitle = "Foundational and Practical Aspects of Resource Analysis: - Second International Workshop, {FOPARA} 2011", + Second International Workshop (FOPARA 2011), + Revised Selected Papers", Editor = "R. Pe\~{n}a and M. {van Eekelen} and O. Shkaravska", Address = "Madrid, Spain", Pages = "36--53", @@ -4255,7 +4258,7 @@ Summarizing: Journal = "Bioinformatics", Publisher = "Oxford University Press", Volume = 25, - Number = "12", + Number = 12, Pages = "i169--i178", Year = 2009, Note = "Paper accepted for presentation at the 2009 ISMB/ECCB Conference, @@ -5197,7 +5200,8 @@ Summarizing: @Inproceedings{ZanioliFC12, Author = "M. Zanioli and P. Ferrara and A. Cortesi", Title = "{SAILS}: Static Analysis of Information Leakage with Sample", - Booktitle = "Proceedings of the 27th Annual {ACM} Symposium on Applied Computing", + Booktitle = "Proceedings of the 27th Annual ACM Symposium + on Applied Computing", Editor ="C.-C. Hung and J. Hong", Year = 2012, ISBN = "978-1-4503-0857-1",

1 0

[GIT] ppl/ppl(master): Abstracts fixed. Avoided non-ASCII characters.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: 3ccd08df85d78ef507fd2a359251a009559fe110 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3ccd08df85d7… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 11:01:13 2013 +0100 Abstracts fixed. Avoided non-ASCII characters. --- doc/ppl_citations.bib | 18 +++++++++--------- 1 files changed, 9 insertions(+), 9 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 9ef85bc..32e3a39 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -618,14 +618,14 @@ Summarizing: their complicated structures, quantitative time factors and even unknown delays. We present here PSyHCoS, a tool for analyzing parametric real-time systems - specied using the hierarchical modeling language + specified using the hierarchical modeling language PSTCSP. PSyHCoS supports several algorithms for parameter synthesis and model checking, as well as state space reduction techniques. Its architecture favors reusability in terms of syntax, semantics, and algorithms. It comes with a friendly user interface that can be used to edit, simulate and verify PSTCSP - models. Experiments show its eciency and + models. Experiments show its efficiency and applicability." } @@ -1178,7 +1178,7 @@ Summarizing: and J.~Ouaknine. and J.-F.~Raskin and J.~Worrell: On reachability for hybrid automata over bounded time. In: ICALP 2011, Part II. LNCS, vol. 6756, - pp. 416–427. Springer, Heidelberg (2011)] and show that + pp. 416-427. Springer, Heidelberg (2011)] and show that the problem is NExpTime-complete. We also show that we can effectively compute fixed points that characterise the sets of states that are reachable @@ -1401,7 +1401,7 @@ Summarizing: Booktitle = "Quantitative Evaluation of Systems: Proceedings of the 10th International Conference (QEST 2013)", Address = "Buenos Aires, Argentina", - Editor = "K. Joshi and M. Siegle and M. Stoelinga and P. R. D’Argenio", + Editor = "K. Joshi and M. Siegle and M. Stoelinga and P. R. D'Argenio", Year = 2013, Pages = "322--337", Publisher = "Springer-Verlag, Berlin", @@ -3202,8 +3202,8 @@ 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 \leq x \leq h$ or - $l \leq \pm x \pm y \leq h)$ for imperative programs. + 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 @@ -3217,7 +3217,7 @@ Summarizing: 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) \leq \max (x + e, y + f, z + g, h)$), + $\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." } @@ -3472,7 +3472,7 @@ Summarizing: Year = 2013, ISBN = "978-3-319-02443-1 (Print) 978-3-319-02444-8 (Online)", Abstract = "PyEcdar is an open source implementation for reasoning - on timed systems. PyEcdar’s main objective is not + on timed systems. PyEcdar's main objective is not efficiency, but rather flexibility to test and implement new results on timed systems" } @@ -4566,7 +4566,7 @@ Summarizing: verification can be regarded as geometric concepts in machine learning. Safety properties define bad states: states a program should not reach. Program verification - explains why a program’s set of reachable states is + explains why a program's set of reachable states is disjoint from the set of bad states. In Hoare Logic, these explanations are predicates that form inductive assertions. Using samples for reachable and bad states

1 0

[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