Module: ppl/w3ppl Branch: master Commit: 34596d082d31006019a41fed5cbf085fec9b18e4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=34596d082d3...
Author: Roberto Bagnara bagnara@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>