- PPL-devel - BUGSENG Mailman

[GIT] ppl/w3ppl(master): Little improvements: Mazzi and Trabucchi are former students.
by Enea Zaffanella 04 Aug '10

04 Aug '10

Module: ppl/w3ppl Branch: master Commit: c898ecc1e5d35a95ca79936ee12b459e2f81746e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=c898ecc1e5… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Aug 4 14:01:15 2010 +0200 Little improvements: Mazzi and Trabucchi are former students. --- htdocs/Credits/Credits.raw | 12 +++++++----- 1 files changed, 7 insertions(+), 5 deletions(-) diff --git a/htdocs/Credits/Credits.raw b/htdocs/Credits/Credits.raw index 0ee838f..2c84d69 100644 --- a/htdocs/Credits/Credits.raw +++ b/htdocs/Credits/Credits.raw @@ -142,9 +142,9 @@ maintained and improved by the following people: </LI> <LI> Giordano Fracasso - (University of Parma) wrote the initial version - of the support for native and checked integer - coefficients. + (student of the University of Parma) + wrote the initial version of the support for + native and checked integer coefficients. </LI> <LI> Maximiliano Marchesi @@ -154,7 +154,8 @@ maintained and improved by the following people: </LI> <LI> Elena Mazzi - (University of Parma) worked on our implementation + (former student of the University of Parma) + worked on our implementation of bounded differences and octagons. She also participated in the theoretical and practical work concerning widening operators for weakly @@ -192,7 +193,8 @@ maintained and improved by the following people: </LI> <LI> Fabio Trabucchi - (University of Parma) worked on a development + (former student of the University of Parma) + worked on a development branch where he added serializers for all the objects of the PPL. Support for serialization based on Fabio's work, will be available in a

1 0

[GIT] ppl/w3ppl(master): Added a section on exact join detection.
by Roberto Bagnara 04 Aug '10

04 Aug '10

Module: ppl/w3ppl Branch: master Commit: cd96ace3f3f109fd8da4b1b02a32b2062184950c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=cd96ace3f3… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 4 14:59:53 2010 +0200 Added a section on exact join detection. --- htdocs/Documentation/papers.raw | 25 +++++++++++++++++++++++++ 1 files changed, 25 insertions(+), 0 deletions(-) diff --git a/htdocs/Documentation/papers.raw b/htdocs/Documentation/papers.raw index 24efded..25418c1 100644 --- a/htdocs/Documentation/papers.raw +++ b/htdocs/Documentation/papers.raw @@ -198,6 +198,31 @@ and software systems (including the analysis of imperative programs). </TR> </TABLE> +<H3>On Exact Join Detection</H3> + +<TABLE> +<TR valign="top"> +<TD align="right"> +[<A HREF="bibliography#BagnaraHZ10CGTA">BHZ10</A>] +</TD> +<TD> +R. Bagnara, P. M. Hill, and E. Zaffanella. + Exact join detection for convex polyhedra and other numerical + abstractions. + <em>Computational Geometry: Theory and Applications</em>, + 43(5):453-473, 2010. +<BLOCKQUOTE> +Read this paper if you are interested in the theory we developed +for computing the <EM>exact join</EM> predicates provided by +the PPL (exact join detection is the problem of deciding whether +the least upper bound of two or more numerical abstractions is equal +to their set-theoretic union). +</BLOCKQUOTE> +</TD> +</TR> +</TABLE> + + <H3>On the Synthesis of Linear Ranking Functions</H3> <TABLE>

1 0

[GIT] ppl/w3ppl(master): Missing label added.
by Roberto Bagnara 04 Aug '10

04 Aug '10

Module: ppl/w3ppl Branch: master Commit: cadd225c086b58ed038ff25ba0c4d10f55bea374 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=cadd225c08… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 4 14:51:47 2010 +0200 Missing label added. --- htdocs/Documentation/papers.raw | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/htdocs/Documentation/papers.raw b/htdocs/Documentation/papers.raw index bf72d12..24efded 100644 --- a/htdocs/Documentation/papers.raw +++ b/htdocs/Documentation/papers.raw @@ -203,7 +203,7 @@ and software systems (including the analysis of imperative programs). <TR valign="top"> <TD align="right"> -[<A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraMPZ10TR"></A>] +[<A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraMPZ10TR">BMPZ10</A>] </TD> <TD> R. Bagnara, F. Mesnard, A. Pescetti, and E. Zaffanella.

1 0

[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