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@microsoft.com>
Laura Kovacs <lkovacs@complang.tuwien.ac.at>
Posts
