[Om-announce] Second Call for Papers - Special Issue of Journal of Symbolic Computation on Reasoning about Loops

[Laura Kovacs]

[Please post - apologies for multiple copies.]


Second 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: December 13, 2010 
Notification of acceptance: March 14, 2011
Submission of the final accepted version: April 11, 2011 
Publication: Mid of 2011


SCOPE
---------

The ability to extract and synthesize auxiliary properties 
of programs has had a profound effect on program analysis, 
testing and verification over the last several decades. 
The field of invariant generation draws on a multitude 
of techniques ranging from computer algebra, theorem proving, 
constraint solving, abstract interpretation techniques and 
model-checking.
 Likewise, are the application areas diversified from 
bootstrapping static program analysis tools, to test-case 
generation and into aiding the quest for verified software. 
 Yet, invariant generation poses as many challenges as promises:
 A key impediment for program verification is the overhead 
associated with providing, debugging, and verifying auxiliary 
invariant annotations. As the design and implementation of 
reliable software remains an important issue, any progress 
in this area will be of utmost importance for future 
developments in verified software. In the context of static 
analysis and test-case generation, suitable invariants have 
the potential of enabling sophisticated automatic program 
analysis and high-coverage test-case generation.


Several modern techniques for program termination and expected 
program execution time also rely heavily on suitable invariants 
(as relations) for the termination analysis.

Automated discovery of inductive assertions is therefore one 
of the ultimate challenges for verification of safety and 
security properties of programs.


This special issue is related to the topics of the workshop 
WING 2010 (http://research.microsoft.com/en-us/events/wing2010/):
Workshop on Invariant Generation, which took place as a 
sattelite event of FLoC 2010, in Edinburgh, July 21, 2010.
It will  be published by Elsevier within the
Journal of Symbolic Computation.


Both participants of the WING 2010 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,
   - Interpolation
* Tools for inductive assertion generation and verification
* Alternative techniques for reasoning about loops


SUBMISSION GUIDELINES
-------------------

This special issue welcomes original high-quality 
contributions that have been neither published in nor 
simultaneously 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 2010 workshop 
are welcome and encouraged to submit extended and revised 
versions of their papers. Furthermore, submissions of 
papers that are in the scope of WING, but did not appear
in WING 2010 are welcome as well.


Submitted papers must be in English and include a well 
written introduction addressing the following questions 
in succinct and informal manner:
 - What is the problem? 
 - Why is the problem important? 
 - What has been done so far on the problem?
 - What is the main contribution of the paper on the problem?
 - Is the contribution original?     Explain why.
 - Is the contribution non-trivial?  Explain why.
All the main definitions, theorems and algorithms should
be illustrated by simple but meaningful examples.


SUBMISSION
--------------------

Please prepare your submission in LaTeX using the JSC 
document format from: http://www4.ncsu.edu/~hong/jsc.htm.

Submission is via the EasyChair submission site at:
http://www.easychair.org/conferences/?conf=wingjsc2010


GUEST EDITORS
--------------------
Nikolaj Bjorner (Microsoft Research, US)
Laura Kovacs (Vienna University of Technology, Austria)



FURTHER INFORMATION
-------------------------------
Nikolaj Bjorner <nbjorner at microsoft.com>
Laura Kovacs <lkovacs at complang.tuwien.ac.at>