December 2013 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Removed duplicate entry.
by Roberto Bagnara 28 Dec '13

28 Dec '13

Module: ppl/ppl Branch: master Commit: f9ccf58636a2ff7f1f8b911b4acf51ed93eb492d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f9ccf58636a2… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Dec 28 09:01:10 2013 +0100 Removed duplicate entry. --- doc/ppl_citations.bib | 31 ------------------------------- 1 files changed, 0 insertions(+), 31 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 9782924..f00982c 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -824,37 +824,6 @@ Summarizing: special PTIME cases." } -@Article{benerecettiFM13, - Author= "M. Benerecetti and M. Faella and S. Minopoli", - Title = "Automatic synthesis of switching controllers for linear hybrid systems: Safety control", - Journal = "Theoretical Computer Science", - Year = 2013, - Volume = 493, - Pages = "116--138", - DOI = "10.1016/j.tcs.2012.10.042", - Publisher="Elsevier Science B.V.", - Abstract = "In this paper we study the problem of automatically - generating switching con- trollers for the class of - Linear Hybrid Automata, with respect to safety - objectives. While the same problem has been already - considered in the literature, no sound and complete - solution has been provided so far. We identify and solve - inaccuracies contained in previous characterizations of - the problem, providing a sound and complete symbolic - xpoint procedure to compute the set of states from which - a controller can keep the system in a given set of - desired states. While the overall procedure may not - terminate, we prove the termination of each iteration, - thus paving the way to an effective implementation. The - techniques needed to effectively and efficiently - implement the proposed solution procedure, based on - polyhedral abstractions of the state space, are - thoroughly illustrated and discussed. Finally, some - supporting and promising experimental results, based on - the implementation of the proposed techniques on top of - the tool PHAVer, are presented." -} - @Inproceedings{BerendsenJV10, Author = "J. Berendsen and D. N. Jansen and F. W. Vaandrager", Title = "Fortuna: Model Checking Priced Probabilistic Timed Automata",

1 0

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

28 Dec '13

Module: ppl/ppl Branch: master Commit: 375dc91eab14dd1c7cd50c351fd3d3852e21c758 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=375dc91eab14… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Dec 28 09:00:50 2013 +0100 Book title fixed. --- 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 2b3f807..9782924 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -797,14 +797,15 @@ Summarizing: @Inproceedings{Ben-AmramG13, Author = "A. M. Ben-Amram and S. Genaim", - Title = "On the Linear Ranking Problem for Integer Linear-constraint Loops", - Booktitle = "{POPL '13} Proceedings of the 40th Annual {ACM SIGPLAN-SIGACT} Symposium on Principles of Programming Languages", + Title = "On the Linear Ranking Problem for Integer Linear-Constraint Loops", + Booktitle = "Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on + Principles of Programming Languages (POPL 2013)", Year = 2013, ISBN = "978-1-4503-1832-7", Address = "Rome, Italy", Pages = "51--62", Publisher = "ACM Press", - Note = "Also published in ACM SIGPLAN Notices, POPL '13, Volume 48 Issue 1", + Note = "Also published in ACM SIGPLAN Notices, POPL '13, Volume 48, Issue 1", Abstract = "In this paper we study the complexity of the Linear Ranking problem: given a loop, described by linear constraints over a finite set of integer variables, is

1 0

[GIT] ppl/ppl(master): Title fixed and abstract added.
by Roberto Bagnara 28 Dec '13

28 Dec '13

Module: ppl/ppl Branch: master Commit: 0aa1d092fc001b1aa6accad3a78d8fd7c81377e8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0aa1d092fc00… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Dec 28 08:58:20 2013 +0100 Title fixed and abstract added. --- doc/ppl_citations.bib | 26 +++++++++++++++++++++++++- 1 files changed, 25 insertions(+), 1 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index d25ae10..2b3f807 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -581,11 +581,35 @@ Summarizing: @Book{AndreS13, Author = "{\'E}. Andr{\'e} and R. Soulat", - Title = "The Inverse Method: Parametric Verification of Real-time Unbedded Systems", + Title = "The Inverse + Method: Parametric Verification of Real-time Embedded Systems", Publisher = "John Wiley and Sons.", Series = "{FOCUS Series}", ISBN = "9781118569405", Year = 2013, + Abstract = "This book introduces state-of-the-art verification + techniques for real-time embedded systems, based on the + inverse method for parametric timed automata. It reviews + popular formalisms for the specification and + verification of timed concurrent systems and, in + particular, timed automata as well as several extensions + such as timed automata equipped with stopwatches, linear + hybrid automata and affine hybrid automata. The inverse + method is introduced, and its benefits for guaranteeing + robustness in real-time systems are shown. Then, it is + shown how an iteration of the inverse method can solve + the good parameters problem for parametric timed + automata by computing a behavioral cartography of the + system. Different extensions are proposed particularly + for hybrid systems and applications to scheduling + problems using timed automata with stopwatches. Various + examples, both from the literature and industry, + illustrate the techniques throughout the book. Various + parametric verifications are performed, in particular of + abstractions of a memory circuit sold by the chipset + manufacturer ST-Microelectronics, as well as of the + prospective flight control system of the next generation + of spacecraft designed by ASTRIUM Space Transportation." } @Inproceedings{ArmandoBM07,

1 0

[GIT] ppl/ppl(master): Fixed more book titles.
by Roberto Bagnara 28 Dec '13

28 Dec '13

Module: ppl/ppl Branch: master Commit: e4c47c3d6ded048c8fb8bc477beb5fa18ef50088 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e4c47c3d6ded… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Dec 28 08:55:17 2013 +0100 Fixed more book titles. --- doc/ppl_citations.bib | 28 ++++++++++++++++------------ 1 files changed, 16 insertions(+), 12 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 834ea42..d25ae10 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -526,7 +526,7 @@ Summarizing: @Inproceedings{AndreFS13, Author = "{\'E}. Andr{\'e} and L. Fribourg and R. Soulat", Title = "Merge and Conquer: State Merging in Parametric Timed Automata", - Booktitle = "Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis, {ATVA 2013}", + Booktitle = "Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA 2013)", Editor = "D. Van Hung and M. Ogawa", Address = "Hanoi, Vietnam", Pages = "381--396", @@ -555,7 +555,8 @@ Summarizing: Author = "E. Andr{\'e} and Y. Liu and J. Sun and J. S. Dong and {S.-W}. Lin", Title = "PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems", - Booktitle = "Proceedings of Computer Aided Verification - 25th International Conference, {CAV} 2013", + Booktitle = "Computer Aided Verification: + Proceedings of the 25th International Conference (CAV 2013)", Year = 2013, Pages = "984--989", Editor = "N. Sharygina and H. Veith", @@ -1189,7 +1190,8 @@ Summarizing: @Inproceedings{ChakarovS13, Author = "A. Chakarov and S. Sankaranarayanan", Title = "Probabilistic Program Analysis with Martingales", - Booktitle = "Proceedings of Computer Aided Verification - 25th International Conference, {CAV} 2013", + Booktitle = "Computer Aided Verification: + Proceedings of the 25th International Conference (CAV 2013)", Year = 2013, Pages = "511-526", Editor = "N. Sharygina and H. Veith", @@ -2849,11 +2851,11 @@ Summarizing: Author = "B. Jeannet and A. Min{\'e}", Title = "Apron: A Library of Numerical Abstract Domains for Static Analysis", - Booktitle = "Computer Aided Verification, + Booktitle = "Computer Aided Verification: Proceedings of the 21st International Conference (CAV 2009)", Address = "Grenoble, France", Editor = "A. Bouajjani and O. Maler", - Publisher = "Springer", + Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 5643, Pages = "661--667", @@ -2874,14 +2876,16 @@ Summarizing: @Incollection {KhalilGP09, Author = "G. Khalil and E. Goubault and S. Putot", Title = "The Zonotope Abstract Domain {Taylor1+}", - Booktitle = "Computer Aided Verification", - Series = "Lecture Notes in Computer Science", + Booktitle = "Computer Aided Verification: + Proceedings of the 21st International Conference (CAV 2009)", + Address = "Grenoble, France", Editor = "A. Bouajjani and O. Maler", Publisher = "Springer-Verlag, Berlin", - ISBN = "978-3-642-02657-7", - Pages = "627--633", + Series = "Lecture Notes in Computer Science", Volume = 5643, + Pages = "627--633", Year = 2009, + ISBN = "978-3-642-02657-7", Abstract = "Static analysis by abstract interpretation [1] aims it automatically inferring properties on the behaviour of programs. We focus here on a specific kind of numerical @@ -3566,7 +3570,7 @@ Summarizing: @Inproceedings{PerezRS09, Author = "J. A. {Navarro P{\'e}rez} and A. Rybalchenko and A. Singh", Title = "Cardinality Abstraction for Declarative Networking Applications", - Booktitle = "Computer Aided Verification, + Booktitle = "Computer Aided Verification: Proceedings of the 21st International Conference (CAV 2009)", Address = "Grenoble, France", Editor = "A. Bouajjani and O. Maler", @@ -3606,8 +3610,8 @@ Summarizing: @Inproceedings{PhamTTC11, Author = "T.-H. Pham and M.-T. Trinh and A.-H. Truong and W.-N. Chin", Title = "{FixBag:} A Fixpoint Calculator for Quantified Bag Constraints", - Booktitle = "Proceedings of the 23rd International Conference on - Computer Aided Verification (CAV 2011)", + Booktitle = "Computer Aided Verification: + Proceedings of the 23rd International Conference (CAV 2011)", Address = "Snowbird, UT, USA", Series = "Lecture Notes in Computer Science", Editor = "G. Gopalakrishnan and S. Qadeer",

1 0

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

28 Dec '13

Module: ppl/ppl Branch: master Commit: f6149a7984b927ae3941871a5efd3d115b5b314a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f6149a7984b9… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Dec 28 08:47:59 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 7543961..834ea42 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -497,7 +497,8 @@ Summarizing: @Inproceedings{AndreFS12, Author = "{\'E}. Andr{\'e} and L. Fribourg and R. Soulat", Title = "Enhancing the Inverse Method with State Merging", - Booktitle = "Proceedings of the 4th International Symposium on {NASA} Formal Methods, {NFM} 2012", + Booktitle = "NASA Formal Methods: + Proceedings of the 4th International Symposium (NFM 2012)", Editor = "A. E. Goodloe and S. Person", Address = "Norfolk, USA", Pages = "381--396",

1 0

[GIT] ppl/ppl(master): Fixed several typos.
by Roberto Bagnara 28 Dec '13

28 Dec '13

Module: ppl/ppl Branch: master Commit: cdb6ec47f9cb79e3b3d8af4aee9b8c4c97195e5e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cdb6ec47f9cb… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sat Dec 28 08:43:25 2013 +0100 Fixed several typos. --- doc/ppl_citations.bib | 22 ++++++++++++---------- 1 files changed, 12 insertions(+), 10 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index d6f4673..7543961 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -190,18 +190,18 @@ Summarizing: } @Article{AlbertGM13, - Author = "E. Albert and S. Genaim and A. N. Masud", - Title = "On the Inference of Resource Usage Upper and Lower Bounds", - Journal = "ACM Transactions on Computational Logic (TOCL)", - Volume = 14, - Number = 3, - Year = 2013, + Author = "E. Albert and S. Genaim and A. N. Masud", + Title = "On the Inference of Resource Usage Upper and Lower Bounds", + Journal = "ACM Transactions on Computational Logic", + Volume = 14, + Number = 3, + Year = 2013, Abstract = "Cost analysis aims at determining the amount of resources required to run a program in terms of its input data sizes. The most challenging step is to infer the cost of executing the loops in the program. This requires bounding the number of iterations of each loop - and finding tight bounds for the cost of each of its + and findig tight bounds for the cost of each of its iterations. This article presents a novel approach to infer upper and lower bounds from cost relations. These relations are an extended form of standard recurrence @@ -258,8 +258,10 @@ Summarizing: @Inproceedings{AlthoffK12, Author = "M. Althoff and B. H. Krogh", - Title = "Avoiding Geometric Intersection Operations in Reachability Analysis of Hybrid Systems", - Booktitle = "Proceedings of the 15th {ACM} International Conference on Hybrid Systems: Computation and Control, (HSCC '12)", + Title = "Avoiding Geometric Intersection Operations + in Reachability Analysis of Hybrid Systems", + Booktitle = "Proceedings of the 15th ACM International Conference + on Hybrid Systems: Computation and Control (HSCC '12)", Year = 2012, ISBN = "978-1-4503-1220-2", Address = "Beijing, China", @@ -346,7 +348,7 @@ Summarizing: demo model from Mathworks." } -@Inproceedings {AmatoPS10, +@Inproceedings{AmatoPS10, Author = "G. Amato and M. Parton and F. Scozzari", Title = "A Tool Which Mines Partial Execution Traces to Improve Static Analysis",

1 0

[GIT] ppl/ppl(master): Typo fixed.
by Patricia Hill 27 Dec '13

27 Dec '13

Module: ppl/ppl Branch: master Commit: 7b58fb37701d10394c64d8e47e9d09160461f639 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7b58fb37701d… Author: Patricia Hill <patricia.hill(a)bugseng.com> Date: Fri Dec 27 20:52:34 2013 +0000 Typo fixed. --- doc/ppl_citations.bib | 1 - 1 files changed, 0 insertions(+), 1 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index f5061c6..d6f4673 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -4344,7 +4344,6 @@ Summarizing: over previous algorithms. Several open instances could be solved to optimality." } -[download] @Inproceedings{UpadrastaC13, Author = "R. Upadrasta and A. Cohen",

1 0

[GIT] ppl/ppl(master): Typo fixed.
by Patricia Hill 27 Dec '13

27 Dec '13

Module: ppl/ppl Branch: master Commit: 41b13b75c6624df839fef8caa38b2a1856c785e5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=41b13b75c662… Author: Patricia Hill <patricia.hill(a)bugseng.com> Date: Fri Dec 27 20:50:08 2013 +0000 Typo 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 793cc82..f5061c6 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -4605,7 +4605,7 @@ Summarizing: ============================================================================== <h2>ODC Attribution License (ODC-By)</h2> -and, + ### Preamble The Open Data Commons Attribution License is a license agreement

1 0

[GIT] ppl/ppl(master): Added recently published papers citing the PPL.
by Patricia Hill 27 Dec '13

27 Dec '13

Module: ppl/ppl Branch: master Commit: e1501ba3dbd83ff1aeb51090b902c969b8f71da0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e1501ba3dbd8… Author: Patricia Hill <patricia.hill(a)bugseng.com> Date: Fri Dec 27 20:35:31 2013 +0000 Added recently published papers citing the PPL. Added papers are books, journal articles or conference proceedings published in 2012-2013 that cite "The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems." Theses, workshop papers and technical reports have not been added in this commit. --- doc/ppl_citations.bib | 766 ++++++++++++++++++++++++++++++++++++++++++++++++- 1 files changed, 764 insertions(+), 2 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=e1501ba3…

1 0

Out of memory when solving integer problem with only two large vars
by Georgi Guninski 23 Dec '13

23 Dec '13

I am trying to solve the following problem, not necessarily with ppl. Given positive integers $A0,B0,L$ find integers $A,B$ satisfying: 1 <= A A <= L 1 <= B B <= L 1 <= A0*A - B0*B A0*A - B0*B <= L Encoded it in PPL by modifying an example (also attached): ===== Constraint_System cs; cs.insert(A >= 1); cs.insert(A <= Coefficient(L)); cs.insert(B >= 1); cs.insert(B <= Coefficient(L)); cs.insert(Coefficient(A0)*A - Coefficient(B0)*B >= 1); cs.insert(Coefficient(A0)*A - Coefficient(B0)*B <= Coefficient(L) ); // All integer variables. Variables_Set ivs(A, B); // Cost function. Linear_Expression cost(Coefficient("10")); MIP_Problem mip(cs.space_dimension(), cs.begin(), cs.end(), ivs, cost, MINIMIZATION); if (mip.solve() != OPTIMIZED_MIP_PROBLEM) { ======= (reads 3 ints from stdin) This works for small input, but for: A0=654013667618 B0=654013667619 L=808711 PPL consumes 6GB RAM very fast and I run out of memory. Am I doing something wrong? Other ways to solve the problem? Attached is the source, function "test10". Thank you. ppl-1.1 on x86_64 linux. -- Georgi

3 5