Proving termination is a central problem in software development
and formal methods for termination analysis are required for program
verification. Therefore, techniques for automated termination proofs
are essential for mechanized reasoning about computations.
While methods for automated termination analysis have been
studied for decades, recently many new results have been achieved
in this area leading to the development of new and powerful automated
The aim of this special issue is to present the most recent advances
in the automation of termination proofs. The scope of the issue
includes termination of any kind of computation (e.g., term rewriting,
logic programming, functional programming, imperative programming, etc.).
Authors are invited to submit full papers describing original results
not published elsewhere. Moreover, the submission of enhanced versions
of conference papers is also acceptable provided that the version
submitted contains sufficient additional results, discussion, examples,
or proofs. We also encourage the submission of system descriptions and
of papers containing both the presentation of new techniques for
automated termination proofs and the description of a system where
they are implemented. The submissions will be refereed according
to the usual standards of the Journal of Automated Reasoning.
Electronic submissions (in postscript- or pdf-format) should
be prepared using the style files at
and should be sent to one of the guest editors.
|November 30, 2003
|March 31, 2004
|Publication of the Special Issue: