[WING] 2nd CfP: Special Issue of the JSC on Invariant Generation

[Martin Giese]

[apologies for multiple copies!]


    Second and Final 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: July 1, 2008
Notification of acceptance: November 1, 2008
Publication: First quarter of 2009


      GENERAL INFORMATION

The logically deepest aspect of program verification is to prove
properties of loops, respectively recursive programs. 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, that
are based on techniques ranging from polynomial algebra to abstract
interpretation.

This special issue has its origins in the Workshop on Invariant
Generation which was held in Hagenberg (Austria) in June 2007. It will
be published by Elsevier within the Journal of Symbolic Computation.


      TOPICS

This special issue focuses on advanced techniques for proving properties of
programs with loops or recursion. Topics of interest include but are not
limited to the following:

    * Analysis and verification of programs with loops and recursion
    * Inductive assertion generation
    * Inductive proofs for reasoning about loops
    * Applications to assertion generation using the following tools:
          o Algebraic techniques
          o Abstract interpretation
          o Static analysis
          o Model checking
          o Theorem proving
    * 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 2007 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
martingi@ifi.uio.no


      GUEST EDITORS

Martin Giese (University of Oslo, Norway)
Tudor Jebelean (Research Institute for Symbolic Computation, Hagenberg,
Austria)


      FURTHER INFORMATION

martingi@ifi.uio.no
tjebelea@risc.uni-linz.ac.at