[PPL-devel] [GIT] ppl/w3ppl(master): Added BozgaGI09.

[Roberto Bagnara]

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

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Sun Mar  7 19:23:29 2010 +0400

Added BozgaGI09.

---

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

diff --git a/htdocs/Documentation/ppl_citations.bib b/htdocs/Documentation/ppl_citations.bib
index a83eb79..e51ce00 100644
--- a/htdocs/Documentation/ppl_citations.bib
+++ b/htdocs/Documentation/ppl_citations.bib
@@ -346,6 +346,44 @@
               a basis for an implementation of our representation."
 }
 
+ at Inproceedings{BozgaGI09,
+  Author = "M. Bozga and C. G\^{\i}rlea and R. Iosif",
+  Title = "Iterating Octagons",
+  Booktitle = "Proceedings of the 15th International Conference on
+               Tools and Algorithms for the Construction and Analysis
+               of Systems (TACAS 2009)",
+  Address = "York, UK",
+  Editor = "S. Kowalewski and A. Philippou",
+  Publisher = "Springer-Verlag, Berlin",
+  Series = "Lecture Notes in Computer Science",
+  Volume = 5505,
+  Pages = "337-351",
+  Year = 2009,
+  ISBN = "978-3-642-00767-5",
+  Abstract = "In this paper we prove that the transitive closure of a
+              nondeterministic octagonal relation using integer
+              counters can be expressed in Presburger arithmetic. The
+              direct consequence of this fact is that the reachability
+              problem is decidable for flat counter automata with
+              octagonal transition relations. This result improves the
+              previous results of Comon and Jurski [Hubert Comon and
+              Yan Jurski. Multiple counters automata, safety analysis
+              and presburger arithmetic. In \emph{CAV}, LNCS 1427, pages
+              268–279, 1998] and Bozga, Iosif and Lakhnech [Marius Bozga,
+              Radu Iosif, and Yassine Lakhnech. Flat parametric counter
+              automata. In \emph{ICALP}, LNCS 4052, pages 577–588.
+              Springer-Verlag, 2006] concerning the computation of
+              transitive closures for difference bound relations.
+              The importance of this result is justified by the wide
+              use of octagons to computing sound abstractions of
+              real-life systems [A. Min\'e. The octagon abstract domain.
+              \emph{Higher-Order and Symbolic Computation}, 19(1):31–100,
+              2006]. We have implemented the octagonal transitive closure
+              algorithm in a prototype system for the analysis of counter
+              automata, called FLATA, and we have experimented with a
+              number of test cases."
+}
+
 @Inproceedings{BramanM08,
   Title = "Safety Verification of Fault Tolerant Goal-based Control Programs
            with Estimation Uncertainty",