August 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/w3ppl(master): Redone the part on the synthesis of linear ranking functions.
by Roberto Bagnara 04 Aug '10

04 Aug '10

Module: ppl/w3ppl Branch: master Commit: 701b4390c86269ce0904cf796c57eedb51dccf86 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=701b4390c8… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 4 14:49:52 2010 +0200 Redone the part on the synthesis of linear ranking functions. Only cite published papers. Do not just replicate the abstract. --- htdocs/Documentation/papers.raw | 34 +++++++++++++--------------------- 1 files changed, 13 insertions(+), 21 deletions(-) diff --git a/htdocs/Documentation/papers.raw b/htdocs/Documentation/papers.raw index 5a98265..bf72d12 100644 --- a/htdocs/Documentation/papers.raw +++ b/htdocs/Documentation/papers.raw @@ -198,7 +198,7 @@ and software systems (including the analysis of imperative programs). </TR> </TABLE> -<H3>On Linear Ranking Functions</H3> +<H3>On the Synthesis of Linear Ranking Functions</H3> <TABLE> <TR valign="top"> @@ -206,28 +206,20 @@ and software systems (including the analysis of imperative programs). [<A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraMPZ10TR"></A>] </TD> <TD> -R. Bagnara, F. Mesnard, F. Pescetti, and E. Zaffanella. - The Automatic Synthesis of Linear Ranking Functions. - Submitted for publication, 2010.<BR> +R. Bagnara, F. Mesnard, A. Pescetti, and E. Zaffanella. + The automatic synthesis of linear ranking functions: The complete + unabridged version. + Quaderno 498, Dipartimento di Matematica, Università di Parma, + Italy, 2010. + Available at <A HREF="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</A>. + Also published as <TT>arXiv:cs.PL/1004.0944</TT>, available from + <A HREF="http://arxiv.org/">http://arxiv.org/</A>. <BLOCKQUOTE> Read this paper if you are interested in synthesizing ranking -functions for termination analysis. The classical technique for -proving termination of a generic sequential computer program involves -the synthesis of a <EM>ranking function</EM> for each loop of the -program. <EM>Linear</EM> ranking functions are particularly -interesting because many terminating loops admit one and algorithms -exist to automatically synthesize it. In this paper we present two -such algorithms: one based on work dated 1991 by Sohn and Van~Gelder; -the other, due to Podelski and Rybalchenko, dated 2004. Remarkably, -while the two algorithms will synthesize a linear ranking function -under exactly the same set of conditions, the former is mostly unknown -to the community of termination analysis and its general applicability -has never been put forward before the present paper. In this paper we -thoroughly justify both algorithms, we prove their correctness, we -compare their worst-case complexity and experimentally evaluate their -efficiency, and we present an open-source implementation of them that -will make it very easy to include termination-analysis capabilities in -automatic program verifiers. +functions for termination analysis. The two methods presented in this +paper are fully implemented in the PPL and make it very easy to +include termination-analysis capabilities in automatic program +verifiers. </BLOCKQUOTE> </TD> </TR>

1 0

[GIT] ppl/w3ppl(master): Avoid just repeating the title.
by Roberto Bagnara 04 Aug '10

04 Aug '10

Module: ppl/w3ppl Branch: master Commit: b0065bc94144823bcc4ac5be2bb1f6c63d4cfc74 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=b0065bc941… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 4 14:44:17 2010 +0200 Avoid just repeating the title. --- htdocs/Documentation/papers.raw | 7 ++++--- 1 files changed, 4 insertions(+), 3 deletions(-) diff --git a/htdocs/Documentation/papers.raw b/htdocs/Documentation/papers.raw index e2847db..5a98265 100644 --- a/htdocs/Documentation/papers.raw +++ b/htdocs/Documentation/papers.raw @@ -175,7 +175,7 @@ widening operators. </TR> </TABLE> -<H3>On Applications</H3> +<H3>On Applications of Polyhedral Computations</H3> <TABLE> <TR valign="top"> @@ -190,8 +190,9 @@ R. Bagnara, P. M. Hill, and E. Zaffanella. 410(46):4672-4691, 2009.<BR> <BLOCKQUOTE> Read this paper if you are interested in applications of polyhedral -computations to the analysis and verification of hardware and -software systems. +computations (such as the ones supported by the PPL) to the analysis +and verification of hardware (yes, both of digital and analog devices) +and software systems (including the analysis of imperative programs). </BLOCKQUOTE> </TD> </TR>

1 0

[GIT] ppl/w3ppl(master): Fixed misplaced </TABLE>.
by Roberto Bagnara 04 Aug '10

04 Aug '10

Module: ppl/w3ppl Branch: master Commit: 40bc8f5ee67d128e41ceb5715cfb4ca3fc481bd3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=40bc8f5ee6… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 4 12:23:34 2010 +0200 Fixed misplaced </TABLE>. --- htdocs/Documentation/papers.raw | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/htdocs/Documentation/papers.raw b/htdocs/Documentation/papers.raw index ef793be..e2847db 100644 --- a/htdocs/Documentation/papers.raw +++ b/htdocs/Documentation/papers.raw @@ -400,6 +400,8 @@ of the paper [<A HREF="bibliography#BagnaraHZ05STTT">BHZ05b</A>]. </BLOCKQUOTE> </TD> </TR> +</TABLE> + <H3>On Weakly Relational Domains</H3> <TABLE> @@ -422,5 +424,3 @@ weakly relational domains. </TD> </TR> </TABLE> - -</TABLE>

1 0

[GIT] ppl/w3ppl(master): Section names made more specific.
by Roberto Bagnara 04 Aug '10

04 Aug '10

Module: ppl/w3ppl Branch: master Commit: e84c6a711aa6a5304e8fc3c7af90998b7f074cd5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=e84c6a711a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 4 12:21:56 2010 +0200 Section names made more specific. --- htdocs/Documentation/papers.raw | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/htdocs/Documentation/papers.raw b/htdocs/Documentation/papers.raw index f062979..ef793be 100644 --- a/htdocs/Documentation/papers.raw +++ b/htdocs/Documentation/papers.raw @@ -87,7 +87,7 @@ the descriptions of NNC polyhedra. </TR> </TABLE> -<H3>On Widenings</H3> +<H3>On Widenings for Generic Convex Polyhedra</H3> <TABLE> @@ -337,7 +337,7 @@ This technical report is a preliminary version of the paper </TR> </TABLE> -<H3>On Widenings</H3> +<H3>On Widenings for Generic Convex Polyhedra</H3> <TABLE> <TR valign="top">

1 0

[GIT] ppl/w3ppl(master): The current reference for weakly-relational domains is BHZ09FMSD.
by Roberto Bagnara 04 Aug '10

04 Aug '10

Module: ppl/w3ppl Branch: master Commit: 0bc52a61563b420868c49086b27421530a10dc37 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=0bc52a6156… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 4 12:20:26 2010 +0200 The current reference for weakly-relational domains is BHZ09FMSD. --- htdocs/Documentation/papers.raw | 53 ++++++++++++++++++++++----------------- 1 files changed, 30 insertions(+), 23 deletions(-) diff --git a/htdocs/Documentation/papers.raw b/htdocs/Documentation/papers.raw index 24fc6d6..f062979 100644 --- a/htdocs/Documentation/papers.raw +++ b/htdocs/Documentation/papers.raw @@ -153,15 +153,13 @@ previously known (this instance is also fully supported by the PPL). <TR valign="top"> <TD align="right"> -[<A HREF="http://www.cs.unipr.it/ppl/Documentation#BagnaraHMZ05">BHMZ05b</A>] +[<A HREF="bibliography#BagnaraHZ09FMSD">BHZ09FMSD</A>] </TD> <TD> -R. Bagnara, P. M. Hill, E. Mazzi, and E. Zaffanella. - Widening operators for weakly-relational numeric abstractions. - In C. Hankin and I. Silveroni, editors, <EM>Static Analysis: - Proceedings of the 12th International Symposium</EM>, volume 3672 of <EM>Lecture - Notes in Computer Science</EM>, pages 3-18, London, UK, 2005. Springer-Verlag, - Berlin.<BR> +R. Bagnara, P. M. Hill, and E. Zaffanella. + Weakly-Relational Shapes for Numeric Abstractions: Improved + Algorithms and Proofs of Correctness. + <EM>Formal Methods in System Design</EM>, 35(3):(279-323), 2009.<BR> <BLOCKQUOTE> Read this paper if you are interested in using the <EM>weakly relational</EM> domains (the PPL supports the weakly @@ -169,22 +167,9 @@ relational domains of bounded difference shapes and octagonal shapes). These are domains for numerical abstractions that lie between (in terms of precision and efficiency) the domains of intervals and convex polyhedra. -</BLOCKQUOTE> -</TD> -</TR> - -<TR valign="top"> -<TD align="right"> -[<A HREF="bibliography#BagnaraHZ09FMSD">BHZ09FMSD</A>] -</TD> -<TD> -R. Bagnara, P. M. Hill, and E. Zaffanella. - Weakly-Relational Shapes for Numeric Abstractions: Improved - Algorithms and Proofs of Correctness. - <EM>Formal Methods in System Design</EM>, 35(3):(279-323), 2009.<BR> -<BLOCKQUOTE> -This is the paper to read if you are interested in how we implement -the weakly relational domains. +The variants provided by the PPL and described in this paper have several +advantages, including algorithms of reduced complexity and provably correct +widening operators. </BLOCKQUOTE> </TD> </TR> @@ -416,4 +401,26 @@ of the paper [<A HREF="bibliography#BagnaraHZ05STTT">BHZ05b</A>]. </TD> </TR> +<H3>On Weakly Relational Domains</H3> +<TABLE> + +<TR valign="top"> +<TD align="right"> +[<A HREF="http://www.cs.unipr.it/ppl/Documentation#BagnaraHMZ05">BHMZ05b</A>] +</TD> +<TD> +R. Bagnara, P. M. Hill, E. Mazzi, and E. Zaffanella. + Widening operators for weakly-relational numeric abstractions. + In C. Hankin and I. Silveroni, editors, <EM>Static Analysis: + Proceedings of the 12th International Symposium</EM>, volume 3672 of <EM>Lecture + Notes in Computer Science</EM>, pages 3-18, London, UK, 2005. Springer-Verlag, + Berlin.<BR> +<BLOCKQUOTE> +This paper contains our original proposal to use <EM>semantic</EM> +weakly relational domains. +</BLOCKQUOTE> +</TD> +</TR> +</TABLE> + </TABLE>

1 0

[GIT] ppl/w3ppl(master): Fixed links and punctuation. Avoid replicating the links to the PDF files.
by Roberto Bagnara 04 Aug '10

04 Aug '10

Module: ppl/w3ppl Branch: master Commit: 34596d082d31006019a41fed5cbf085fec9b18e4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=34596d082d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 4 12:09:34 2010 +0200 Fixed links and punctuation. Avoid replicating the links to the PDF files. --- htdocs/Documentation/papers.raw | 76 +++++++++++++++----------------------- 1 files changed, 30 insertions(+), 46 deletions(-) diff --git a/htdocs/Documentation/papers.raw b/htdocs/Documentation/papers.raw index dcc8ed1..24fc6d6 100644 --- a/htdocs/Documentation/papers.raw +++ b/htdocs/Documentation/papers.raw @@ -29,21 +29,33 @@ These can be divided into two categories: <TR valign="top"> <TD align="right"> -[<A HREF="bibliography#BagnaraHZH08SCP">BHZ08b</A>] +[<A HREF="bibliography#BagnaraHZ08SCP">BHZ08b</A>] <TD> R. Bagnara, P. M. Hill, and E. Zaffanella. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. <EM>Science of Computer Programming</EM>, 72(1-2):3-21, 2008. -[<a href="http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ08SCP.pdf">.pdf</a>] <BLOCKQUOTE> This is the paper to read or cite if you are interested in or referring to the Parma Polyhedra Library in general: amongst other things, it explains the aim of the project and the main ideas behind it. +You can use the following BibTeX entry: +<PRE> +@AT@Article{BagnaraHZ08SCP, + Author = "R. Bagnara and P. M. Hill and E. Zaffanella", + Title = "The {Parma Polyhedra Library}: Toward a Complete Set of Numerical + Abstractions for the Analysis and Verification + of Hardware and Software Systems", + Journal = "Science of Computer Programming", + Volume = 72, + Number = "1--2", + Pages = "3--21", + Year = 2008, +} +</PRE> </BLOCKQUOTE> - </TD> </TABLE> @@ -62,7 +74,6 @@ R. Bagnara, P. M. Hill, and E. Zaffanella. method. <EM>Formal Aspects of Computing</EM>, 17(2):222-257, 2005.<BR> <BLOCKQUOTE> - This is the paper to read if you are interested in how we implement NNC polyhedra. It describes how the NNC polyhedra are embedded in a higher dimensional vector space so as to reuse the tools and @@ -70,7 +81,6 @@ techniques of the <EM>double description</EM> method. In particular, it defines a theoretically clean, high-level user interface and the specification of an efficient procedure for removing redundancies from the descriptions of NNC polyhedra. - </BLOCKQUOTE> </TD> @@ -89,9 +99,7 @@ the descriptions of NNC polyhedra. R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. <EM>Science of Computer Programming</EM>, 58(1-2):28-56, 2005.<BR> -[ <A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraHRZ05SCP.pdf">.pdf</A> ] <BLOCKQUOTE> - Read this paper if you are interested in widenings and extrapolations available in the PPL for the domain of convex polyhedra. After introducing the standard widening (methods in the library that are @@ -103,7 +111,6 @@ operator (methods in the library that are based on this widening have the prefix BHRZ03). After presenting the well-known widening delay technique, the <EM>with tokens</EM> technique which is also supported by the PPL, is fully described. - </BLOCKQUOTE> </TD> </TR> @@ -121,9 +128,7 @@ R. Bagnara, P. M. Hill, and E. Zaffanella. Widening operators for powerset domains. <EM>Software Tools for Technology Transfer</EM>, 8(4-5):449-466, 2006.<BR> -[ <A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ06STTT.pdf">.pdf</A> ] <BLOCKQUOTE> - Read this paper if you are interested in using powersets to express disjunctive information. The paper describes the <EM>finite powerset construction</EM> which will upgrade any abstract domain to allow for @@ -138,7 +143,6 @@ tackled successfully. The proposed techniques are illustrated by instantiating the widening methodologies on powersets of convex polyhedra, a domain for which no non-trivial widening operator was previously known (this instance is also fully supported by the PPL). - </BLOCKQUOTE> </TD> </TR> @@ -159,15 +163,12 @@ R. Bagnara, P. M. Hill, E. Mazzi, and E. Zaffanella. Notes in Computer Science</EM>, pages 3-18, London, UK, 2005. Springer-Verlag, Berlin.<BR> <BLOCKQUOTE> - - Read this paper if you are interested in using the <EM>weakly relational</EM> domains (the PPL supports the weakly relational domains of bounded difference shapes and octagonal shapes). These are domains for numerical abstractions that lie between (in terms of precision and efficiency) the domains of intervals and convex polyhedra. - </BLOCKQUOTE> </TD> </TR> @@ -182,10 +183,8 @@ R. Bagnara, P. M. Hill, and E. Zaffanella. Algorithms and Proofs of Correctness. <EM>Formal Methods in System Design</EM>, 35(3):(279-323), 2009.<BR> <BLOCKQUOTE> - This is the paper to read if you are interested in how we implement the weakly relational domains. - </BLOCKQUOTE> </TD> </TR> @@ -204,13 +203,10 @@ R. Bagnara, P. M. Hill, and E. Zaffanella. and Verification of Hardware and Software Systems. <EM>Theoretical Computer Science</EM>, 410(46):4672-4691, 2009.<BR> -[ <A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ09TCS.pdf">.pdf</A> ] <BLOCKQUOTE> - Read this paper if you are interested in applications of polyhedral - computations to the analysis and verification of hardware and - software systems - +computations to the analysis and verification of hardware and +software systems. </BLOCKQUOTE> </TD> </TR> @@ -228,8 +224,6 @@ R. Bagnara, F. Mesnard, F. Pescetti, and E. Zaffanella. The Automatic Synthesis of Linear Ranking Functions. Submitted for publication, 2010.<BR> <BLOCKQUOTE> - - Read this paper if you are interested in synthesizing ranking functions for termination analysis. The classical technique for proving termination of a generic sequential computer program involves @@ -248,7 +242,6 @@ compare their worst-case complexity and experimentally evaluate their efficiency, and we present an open-source implementation of them that will make it very easy to include termination-analysis capabilities in automatic program verifiers. - </BLOCKQUOTE> </TD> </TR> @@ -273,7 +266,6 @@ R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Proceedings of the 9th International Symposium</EM>, volume 2477 of <EM>Lecture Notes in Computer Science</EM>, pages 213-229, Madrid, Spain, 2002. Springer-Verlag, Berlin.<br /> - [<A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraRZH02.pdf">.pdf</A>] <BLOCKQUOTE> This is the first published paper about the Parma Polyhedra Library in general. </BLOCKQUOTE> @@ -292,7 +284,7 @@ R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. <A HREF="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</A>.<BR> <BLOCKQUOTE> This technical report is a preliminary version of the paper -[<A HREF="bibliography#BagnaraRZH02">BRZH02a</A>.] +[<A HREF="bibliography#BagnaraRZH02">BRZH02a</A>]. </BLOCKQUOTE> </TD> </TR> @@ -313,10 +305,9 @@ R. Bagnara, P. M. Hill, and E. Zaffanella. Proceedings of the 3rd Workshop on Automated Verification of Critical Systems</EM>, pages 161-176, Southampton, UK, 2003. Published as TR Number DSSE-TR-2003-2, University of Southampton.<BR> -[ <A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ03a.pdf">.pdf</A> ]<BLOCKQUOTE> -This paper, which was presented at AVoCS 2003, is an earlier version of -the paper -[<A HREF="bibliography#BagnaraHZ05FAC">BHZ05a</A>] +<BLOCKQUOTE> +This paper, which was presented at AVoCS 2003, is an earlier version +of the paper [<A HREF="bibliography#BagnaraHZ05FAC">BHZ05a</A>]. </BLOCKQUOTE> </TD> </TR> @@ -334,9 +325,9 @@ R. Bagnara, P. M. Hill, and E. Zaffanella. Madrid, Spain, 2002. Published as TR Number CLIP4/02.0, Universidad Politécnica de Madrid, Facultad de Informática.<BR> -[ <A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ02a.pdf">.pdf</A> ]<BLOCKQUOTE> +<BLOCKQUOTE> This workshop paper is a preliminary version of the paper -[<A HREF="bibliography#BagnaraHZ03a">BHZ03a</A>.] +[<A HREF="bibliography#BagnaraHZ03a">BHZ03a</A>]. </BLOCKQUOTE> </TD> </TR> @@ -355,7 +346,7 @@ R. Bagnara, P. M. Hill, and E. Zaffanella. Available at <A HREF="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</A>.<BR> <BLOCKQUOTE> This technical report is a preliminary version of the paper -[<A HREF="bibliography#BagnaraHZ03a">BHZ03a</A>.] +[<A HREF="bibliography#BagnaraHZ03a">BHZ03a</A>]. </BLOCKQUOTE> </TD> </TR> @@ -375,10 +366,9 @@ R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. International Symposium</EM>, volume 2694 of <EM>Lecture Notes in Computer Science</EM>, pages 337-354, San Diego, California, USA, 2003. Springer-Verlag, Berlin.<BR> -[ <A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraHRZ03.pdf">.pdf</A> ]<BLOCKQUOTE> +<BLOCKQUOTE> This paper, which was presented at SAS 2003, is an earlier version of -the paper -[<A HREF="bibliography#BagnaraHRZ05SCP">BHRZ05</A>] +the paper [<A HREF="bibliography#BagnaraHRZ05SCP">BHRZ05</A>]. </BLOCKQUOTE> </TD> </TR> @@ -396,11 +386,8 @@ R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. <BLOCKQUOTE> - -This technical report is a preliminary version of -the paper -[<A HREF="bibliography#BagnaraHRZ03">BHRZ03a</A>] - +This technical report is a preliminary version of the paper [<A +HREF="bibliography#BagnaraHRZ03">BHRZ03a</A>]. </BLOCKQUOTE> </TD> </TR> @@ -423,11 +410,8 @@ R. Bagnara, P. M. Hill, and E. Zaffanella. pages 135-148, Venice, Italy, 2003. Springer-Verlag, Berlin.<br /> <BLOCKQUOTE> - -This paper, which was presented at VMCAI 2004, is an earlier version of -the paper -[<A HREF="bibliography#BagnaraHZ05STTT">BHZ05b</A>] - +This paper, which was presented at VMCAI 2004, is an earlier version +of the paper [<A HREF="bibliography#BagnaraHZ05STTT">BHZ05b</A>]. </BLOCKQUOTE> </TD> </TR>

1 0

[GIT] ppl/w3ppl(master): BRZH02a is (of course) no longer a current reference for the PPL.
by Roberto Bagnara 04 Aug '10

04 Aug '10

Module: ppl/w3ppl Branch: master Commit: 95aeed2f9400810369dc2be7e5d8ff3f7fc61d67 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=95aeed2f94… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 4 11:59:35 2010 +0200 BRZH02a is (of course) no longer a current reference for the PPL. --- htdocs/Documentation/papers.raw | 33 +++++++++++++++++++++++---------- 1 files changed, 23 insertions(+), 10 deletions(-) diff --git a/htdocs/Documentation/papers.raw b/htdocs/Documentation/papers.raw index 6547536..dcc8ed1 100644 --- a/htdocs/Documentation/papers.raw +++ b/htdocs/Documentation/papers.raw @@ -29,17 +29,14 @@ These can be divided into two categories: <TR valign="top"> <TD align="right"> -[<A HREF="bibliography#BagnaraRZH02">BRZH02a</A>] +[<A HREF="bibliography#BagnaraHZH08SCP">BHZ08b</A>] <TD> -R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. - Possibly not closed convex polyhedra and the Parma Polyhedra - Library. - In M. V. Hermenegildo and G. Puebla, editors, <EM>Static Analysis: - Proceedings of the 9th International Symposium</EM>, volume 2477 of <EM>Lecture - Notes in Computer Science</EM>, pages 213-229, Madrid, Spain, 2002. - Springer-Verlag, Berlin.<br /> -[ <A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraRZH02.pdf">PDF</A>, - <A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraRZH02.pdf">BibTeX</A> ] +R. Bagnara, P. M. Hill, and E. Zaffanella. + The Parma Polyhedra Library: Toward a complete set of numerical + abstractions for the analysis and verification of hardware and software + systems. + <EM>Science of Computer Programming</EM>, 72(1-2):3-21, 2008. +[<a href="http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ08SCP.pdf">.pdf</a>] <BLOCKQUOTE> This is the paper to read or cite if you are interested in or referring to the Parma Polyhedra Library in general: @@ -267,6 +264,22 @@ automatic program verifiers. <TR valign="top"> <TD align="right"> +[<A HREF="bibliography#BagnaraRZH02">BRZH02a</A>] +<TD> +R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. + Possibly not closed convex polyhedra and the Parma Polyhedra + Library. + In M. V. Hermenegildo and G. Puebla, editors, <EM>Static Analysis: + Proceedings of the 9th International Symposium</EM>, volume 2477 of <EM>Lecture + Notes in Computer Science</EM>, pages 213-229, Madrid, Spain, 2002. + Springer-Verlag, Berlin.<br /> + [<A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraRZH02.pdf">.pdf</A>] +<BLOCKQUOTE> +This is the first published paper about the Parma Polyhedra Library in general. +</BLOCKQUOTE> + +<TR valign="top"> +<TD align="right"> [<A HREF="http://www.cs.unipr.it/ppl/Documentation#BagnaraRZH02TR">BRZH02b</A>] </TD> <TD>

1 0

[GIT] ppl/w3ppl(master): Updated the part about binary distributions.
by Roberto Bagnara 04 Aug '10

04 Aug '10

Module: ppl/w3ppl Branch: master Commit: 5bdc8d6a30982a078a98138ad28dbfec34cda7b9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=5bdc8d6a30… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 4 10:27:07 2010 +0200 Updated the part about binary distributions. We no longer distribute binary packages ourselves. --- htdocs/Download/Download.raw | 20 +++++++++++--------- 1 files changed, 11 insertions(+), 9 deletions(-) diff --git a/htdocs/Download/Download.raw b/htdocs/Download/Download.raw index 17d1351..51e2051 100644 --- a/htdocs/Download/Download.raw +++ b/htdocs/Download/Download.raw @@ -43,7 +43,9 @@ the Parma Polyhedra Library resources (sources, binaries and more). <H3>Binary distributions</H3> <P> -Below is a list of the available PPL binary distributions. +Below is a partial list of the available PPL binary distributions. +Please <A HREF="mailto:ppl-devel@cs.unipr.it">let us know</A> +the ones we are missing. <TABLE BORDER=3 CELLSPACING=3 CELLPADDING=3> <TR> @@ -80,15 +82,9 @@ Below is a list of the available PPL binary distributions. <A HREF="http://packages.debian.org/source/sid/ppl">sid</A> </TD> <TD> - <A HREF="@BASE_DIR@Download/ftp/releases/0.10/fedora/8/">8</A> + <A HREF="http://rpm.pbone.net/index.php3?stat=3&limit=1&srodzaj=1&dl=40&search=ppl&d…"><CODE>rpm.pbone.net</CODE> <BR> - <A HREF="@BASE_DIR@Download/ftp/releases/@PPL_VERSION@/fedora/9/">9</A> - <BR> - <A HREF="@BASE_DIR@Download/ftp/releases/@PPL_VERSION@/fedora/10/">10</A> - <BR> - <A HREF="@BASE_DIR@Download/ftp/releases/@PPL_VERSION@/fedora/11/">11</A> - <BR> - <A HREF="@BASE_DIR@Download/ftp/releases/@PPL_VERSION@/fedora/12/">12</A> + <A HREF="https://admin.fedoraproject.org/pkgdb/acls/name/ppl"><CODE>admin.fedoraproject.org</CODE></A> </TD> <TD> <A HREF="http://packages.gentoo.org/package/dev-libs/ppl">Gentoo</A> @@ -99,11 +95,17 @@ Below is a list of the available PPL binary distributions. <A HREF="http://download.opensuse.org/repositories/devel://gcc/openSUSE_11.0/">11.0</A> <BR> <A HREF="http://download.opensuse.org/repositories/devel://gcc/openSUSE_11.1/">11.1</A> + <BR> + <A HREF="http://download.opensuse.org/repositories/devel://gcc/openSUSE_11.2/">11.2</A> </TD> <TD> <A HREF="http://packages.ubuntu.com/hu/source/intrepid/ppl">Intrepid</A> <BR> <A HREF="http://packages.ubuntu.com/hu/source/jaunty/ppl">Jaunty</A> + <BR> + <A HREF="http://packages.ubuntu.com/hu/source/karmic/ppl">Karmic</A> + <BR> + <A HREF="http://packages.ubuntu.com/hu/source/lucid/ppl">Lucid</A> </TD> <TD> <A HREF="http://pdb.finkproject.org/pdb/package.php/ppl">Fink</A>

1 0

[GIT] ppl/w3ppl(master): Two more papers added: BHZ09FMSD and BHZ09TCS.
by Patricia Hill 04 Aug '10

04 Aug '10

Module: ppl/w3ppl Branch: master Commit: 2a2c83fef9c3a2b77b9bfc18bf66a56aab89e5e9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=2a2c83fef9… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Wed Aug 4 07:51:37 2010 +0100 Two more papers added: BHZ09FMSD and BHZ09TCS. --- htdocs/Documentation/papers.raw | 48 +++++++++++++++++++++++++++++++++++++- 1 files changed, 46 insertions(+), 2 deletions(-) diff --git a/htdocs/Documentation/papers.raw b/htdocs/Documentation/papers.raw index 44aa2f3..6547536 100644 --- a/htdocs/Documentation/papers.raw +++ b/htdocs/Documentation/papers.raw @@ -165,14 +165,58 @@ R. Bagnara, P. M. Hill, E. Mazzi, and E. Zaffanella. Read this paper if you are interested in using the <EM>weakly -relational</EM> domains (at present, the PPL supports the weakly -relational domain of bounded difference shapes). These are domains for +relational</EM> domains (the PPL supports the weakly +relational domains of bounded difference shapes and octagonal shapes). +These are domains for numerical abstractions that lie between (in terms of precision and efficiency) the domains of intervals and convex polyhedra. </BLOCKQUOTE> </TD> </TR> + +<TR valign="top"> +<TD align="right"> +[<A HREF="bibliography#BagnaraHZ09FMSD">BHZ09FMSD</A>] +</TD> +<TD> +R. Bagnara, P. M. Hill, and E. Zaffanella. + Weakly-Relational Shapes for Numeric Abstractions: Improved + Algorithms and Proofs of Correctness. + <EM>Formal Methods in System Design</EM>, 35(3):(279-323), 2009.<BR> +<BLOCKQUOTE> + +This is the paper to read if you are interested in how we implement +the weakly relational domains. + +</BLOCKQUOTE> +</TD> +</TR> +</TABLE> + +<H3>On Applications</H3> + +<TABLE> +<TR valign="top"> +<TD align="right"> +[<A HREF="bibliography#BagnaraHZ09TCS">BHZ09TCS</A>] +</TD> +<TD> +R. Bagnara, P. M. Hill, and E. Zaffanella. + Applications of Polyhedral Computations to the Analysis + and Verification of Hardware and Software Systems. + <EM>Theoretical Computer Science</EM>, + 410(46):4672-4691, 2009.<BR> +[ <A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ09TCS.pdf">.pdf</A> ] +<BLOCKQUOTE> + +Read this paper if you are interested in applications of polyhedral + computations to the analysis and verification of hardware and + software systems + +</BLOCKQUOTE> +</TD> +</TR> </TABLE> <H3>On Linear Ranking Functions</H3>

1 0

[GIT] ppl/w3ppl(master): Updated with paper on linear ranking functions and that the sttp paper
by Patricia Hill 03 Aug '10

03 Aug '10

Module: ppl/w3ppl Branch: master Commit: e3bef523bc4b9767c4dbd5b2bd9afc86c85c9a2c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=e3bef523bc… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Aug 3 21:24:40 2010 +0100 Updated with paper on linear ranking functions and that the sttp paper is now published. Note that the source file address for the paper on linear ranking functions is fictitious and either this should be revised or a pdf version of the paper added at that address. (http://www.cs.unipr.it/ppl/Documentation/BagnaraMPZ10TR) --- htdocs/Documentation/papers.raw | 43 +++++++++++++++++++++++++++++++++++++- 1 files changed, 41 insertions(+), 2 deletions(-) diff --git a/htdocs/Documentation/papers.raw b/htdocs/Documentation/papers.raw index c4444be..44aa2f3 100644 --- a/htdocs/Documentation/papers.raw +++ b/htdocs/Documentation/papers.raw @@ -122,8 +122,9 @@ supported by the PPL, is fully described. <TD> R. Bagnara, P. M. Hill, and E. Zaffanella. Widening operators for powerset domains. - <EM>Software Tools for Technology Transfer</EM>, 2005. - To appear.<BR> + <EM>Software Tools for Technology Transfer</EM>, + 8(4-5):449-466, 2006.<BR> +[ <A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ06STTT.pdf">.pdf</A> ] <BLOCKQUOTE> Read this paper if you are interested in using powersets to express @@ -174,6 +175,44 @@ efficiency) the domains of intervals and convex polyhedra. </TR> </TABLE> +<H3>On Linear Ranking Functions</H3> +<TABLE> + +<TR valign="top"> +<TD align="right"> +[<A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraMPZ10TR"></A>] +</TD> +<TD> +R. Bagnara, F. Mesnard, F. Pescetti, and E. Zaffanella. + The Automatic Synthesis of Linear Ranking Functions. + Submitted for publication, 2010.<BR> +<BLOCKQUOTE> + + +Read this paper if you are interested in synthesizing ranking +functions for termination analysis. The classical technique for +proving termination of a generic sequential computer program involves +the synthesis of a <EM>ranking function</EM> for each loop of the +program. <EM>Linear</EM> ranking functions are particularly +interesting because many terminating loops admit one and algorithms +exist to automatically synthesize it. In this paper we present two +such algorithms: one based on work dated 1991 by Sohn and Van~Gelder; +the other, due to Podelski and Rybalchenko, dated 2004. Remarkably, +while the two algorithms will synthesize a linear ranking function +under exactly the same set of conditions, the former is mostly unknown +to the community of termination analysis and its general applicability +has never been put forward before the present paper. In this paper we +thoroughly justify both algorithms, we prove their correctness, we +compare their worst-case complexity and experimentally evaluate their +efficiency, and we present an open-source implementation of them that +will make it very easy to include termination-analysis capabilities in +automatic program verifiers. + +</BLOCKQUOTE> +</TD> +</TR> +</TABLE> + <HR> <A NAME="historical">

1 0