Module: ppl/w3ppl Branch: master Commit: 62da5b310035206635d82a0a0e688af5a525f4c1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=62da5b31003...

Author: Enea Zaffanella zaffanella@cs.unipr.it Date: Tue Apr 7 15:54:08 2009 +0200

Added bibtex entry for BagnaraHZ09 (submitted for publication).

---

htdocs/Documentation/ppl.bib | 35 +++++++++++++++++++++++++++++++++++ 1 files changed, 35 insertions(+), 0 deletions(-)

diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib index 56b4e40..2784df5 100644 --- a/htdocs/Documentation/ppl.bib +++ b/htdocs/Documentation/ppl.bib @@ -896,6 +896,41 @@ URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ09TCS.pdf" }

+@Unpublished{BagnaraHZ09, + Author = "R. Bagnara and P. M. Hill and E. Zaffanella", + Title = "Weakly-Relational Shapes for Numeric Abstractions: Improved + Algorithms and Proofs of Correctness", + Year = 2009, + Note = "Submitted for publication", + Abstract = "Weakly-relational numeric constraints provide a + compromise between complexity and expressivity that is + adequate for several applications in the field of formal + analysis and verification of software and hardware systems. + We address the problems to be solved for the construction + of full-fledged, efficient and provably correct abstract + domains based on such constraints. We first propose to work + with \emph{semantic} abstract domains, whose elements are + \emph{geometric shapes}, instead of the (more concrete) + syntactic abstract domains of constraint networks and + matrices on which the previous proposals are based. + This allows to solve, once and for all, the problem whereby + \emph{closure by entailment}, a crucial operation for the + realization of such domains, seemed to impede the + realization of proper widening operators. In our approach, + the implementation of widenings relies on the availability + of an effective reduction procedure for the considered + constraint description: one for the domain of \emph{bounded + difference shapes} already exists in the literature; we + provide algorithms for the significantly more complex cases + of rational and integer \emph{octagonal shapes}. + We also improve upon the state-of-the-art by presenting, + along with their proof of correctness, closure by entailment + algorithms of reduced complexity for domains based on + rational and integer octagonal constraints. + The consequences of implementing weakly-relational numerical + domains with floating point numbers are also discussed.", +} + @InProceedings{BalasundaramK89, Author = "V. Balasundaram and K. Kennedy", Title = "A Technique for Summarizing Data Access