[ecoop-info] 1st CFP - Special Issue of the JSC on Invariant Generation

[Laura Kovacs]

[Please post - apologies for multiple copies.]


First Call for Papers

--------------------------
Special issue of the

JOURNAL OF SYMBOLIC COMPUTATION

on

INVARIANT GENERATION

and

ADVANCED TECHNIQUES FOR REASONING ABOUT LOOPS
--------------------------

IMPORTANT DATES

Paper submission: September 1, 2009
Notification of acceptance: December 1, 2009
Submssion of the final accepted version: Jan 4, 2009
Publication: First quarter of 2010


SCOPE
---------
Loops and recursion remain key challenges for program 
verification research. While most systems concerned with 
program verification deal with loops by loop invariants
or induction hypotheses that have to be provided by a
human, a number of interesting alternative approaches 
have emerged. Especially promising breakthroughs are 
tecniques based on Groebner bases, quantifier elimination, 
and algorithmic combinatorics, which can be used
in conjunction with model checking, theorem proving, static
analysis and abstract interpretation.


This special issue is related to the topics of the 
workshop WING'09 (http://mtc.epfl.ch/events/WING09/):
Workshop on Invariant Generation,
which took place as a sattelite event of ETAPS 2009,
in York, March 28, 2009.
It will  be published by Elsevier within the 
Journal of Symbolic Computation.


Both participants of the WING'09 workshop and other 
authors are invited to submit contributions.


TOPICS
----------
This special issue focuses on advanced techniques for proving 
properties of programs with loops or recursion.

Relevant topics include (but are not limited to) the following:

* Program analysis and verification
* Inductive Assertion Generation
* Inductive Proofs for Reasoning about Loops
* Applications to Assertion Generation using the following tools:
   - Abstract Interpretation,
   - Static Analysis,
   - Model Checking,
   - Theorem Proving,
   - Algebraic Techniques
* Tools for inductive assertion generation and verification
* Alternative techniques for reasoning about loops


SUBMISSIONS
-------------------

This special issue welcomes original high-quality contributions 
that have been neither published in nor submitted to any journals 
or refereed conferences.  Submissions will be peer-reviewed using 
the standard refereeing procedure of the Journal of Symbolic Computation.

Authors of papers presented at the WING'09 workshop are welcome to
submit extended and revised versions of their papers.  However, other
submission are welcome as well.

Please prepare your submission in LaTeX using the JSC document
format from: http://www4.ncsu.edu/~hong/jsc.htm and send it as a
Postscript or PDF file to

     laura.kovacs at epfl.ch

and 

     A.Ireland at hw.ac.uk





GUEST EDITORS
--------------------
Martin Giese (University of Oslo, Norway)
Andrew Ireland (Heriot-Watt University, UK)
Laura Kovacs (EPFL, Switzerland)


FURTHER INFORMATION
-------------------------------
Laura Kovacs <laura.kovacs at epfl.ch>
Andrew Ireland <A.Ireland at hw.ac.uk>