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