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