Call for Papers
                                      
               Special Issue On Operating Systems Verification
                                      
                       Journal of Automated Reasoning



Industrial-strength software analysis and verification has advanced in recent
years through the introduction of model checking, automated and interactive
theorem proving, static analysis techniques, as well as correctness by
design. However, many techniques are working under restrictive assumptions
which are invalidated by complex (embedded) system software such as operating
system kernels, low-level device drivers or microcontroller code.

This special issue will be devoted to the formal verification of operating
systems and similar low-level systems code. The emphasis is on techniques and
methods that provide real solutions to real software problems. A real
solution is one that is applicable to the problem in industry and not one
that only applies to an abstract, academic toy version of it. Submissions are
encouraged, but not limited to, the following topics and their application to
operating systems or low-level systems code:

    * model checking
    * automated and interactive theorem proving
    * embedded systems development
    * programming languages
    * verifying compilers
    * software certification

Manuscripts should be unpublished works and not submitted elsewhere. Revised
and enhanced versions of papers published in conference proceedings that have
not appeared in archival journals are eligible for submission. All
submissions will be reviewed according to the usual standards of scholarship
and originality.

Papers should be in pdf format, following the JAR guidelines for authors, and
be submitted via EasyChair at:
            http://www.easychair.org/conferences/?conf=jarosv08 

Please do not use the Springer online submission system for the special issue
at this stage, but EasyChair instead. To encourage a speedy review cycle, it
will be expected that authors of submissions also serve as referees. We encourage
authors to keep their submissions below 30 pages.

For more information, please see 
                http://www.cse.unsw.edu.au/~kleing/JAR-OSV-08/

Guest Editors
Gerwin Klein, NICTA, Australia, gerwin.klein at nicta.com.au
Ralf Huuck, NICTA, Australia, ralf.huuck at nicta.com.au
Bastian Schlich, RWTH Aachen, Germany, schlich at cs.rwth-aachen.de

Important Dates
Sep 29 2008    Submission Deadline (extended)
Dec 15 2008    Notification of accepted papers
Jan 15 2009    Final version