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

[Roberto Bagnara]

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

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Sat Apr 11 20:48:55 2009 +0200

Added AlbertACGPZ08.

---

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

diff --git a/htdocs/Documentation/ppl_citations.bib b/htdocs/Documentation/ppl_citations.bib
index 6aa14f7..aec1454 100644
--- a/htdocs/Documentation/ppl_citations.bib
+++ b/htdocs/Documentation/ppl_citations.bib
@@ -1,3 +1,38 @@
+ at Inproceedings{AlbertACGPZ08,
+  Author = "E. Albert and P. Arenas and M. Codish and S. Genaim
+            and G. Puebla and D. Zanardini",
+  Title = "Termination Analysis of {Java} {Bytecode}",
+  Booktitle = "Proceedings of the 10th IFIP WG 6.1 International Conference
+               on Formal Methods for Open Object-Based Distributed Systems
+               (FMOODS 2008)",
+  Address = "Oslo, Norway",
+  Editor = "G. Barthe and F. S. de Boer",
+  Publisher = "Springer-Verlag, Berlin",
+  Series = "Lecture Notes in Computer Science",
+  Volume = 5051,
+  Year = 2008,
+  Pages = "2--18",
+  ISBN = "978-3-540-68862-4",
+  Abstract = "Termination analysis has received considerable
+              attention, traditionally in the context of declarative
+              programming, and recently also for imperative
+              languages. In existing approaches, termination is
+              performed on source programs. However, there are many
+              situations, including mobile code, where only the
+              compiled code is available. In this work we present an
+              automatic termination analysis for sequential Java
+              Bytecode programs. Such analysis presents all of the
+              challenges of analyzing a low-level language as well as
+              those introduced by object-oriented languages.
+              Interestingly, given a bytecode program, we produce a
+              \emph{constraint logic program}, CLP, whose termination
+              entails termination of the bytecode program. This allows
+              applying the large body of work in termination of CLP
+              programs to termination of Java bytecode. A prototype
+              analyzer is described and initial experimentation is
+              reported."
+}
+
 @Inproceedings{AlbertAGP08,
   Author = "E. Albert and P. Arenas and S. Genaim and G. Puebla",
   Title = "Automatic Inference of Upper Bounds for Recurrence Relations