[Haskell] SVV'05 CFP: INTERNATIONAL WORKSHOP ON SOFTWARE VERIFICATION AND VALIDATION

[Zijiang (James) Yang]

--------------------------------------------------------------------------------
                            CALL FOR PAPERS

                   SVV'05: 3RD INTERNATIONAL WORKSHOP ON 
                   SOFTWARE VERIFICATION AND VALIDATION
                              October 31, 2005
                               Manchester, UK
                 http://www.cs.wmich.edu/~zijiang/svv2005/

                              In Conjunction with
           International Conference on Formal Engineering Methods	           
                                (ICFEM'05)

--------------------------------------------------------------------------------


Goal of the Workshop

Software is playing an important role in economy, government, and military. 
Since software is often deployed in safety critical applications, correctness 
and reliability have become issues of utmost importance. Techniques for 
verification and validation traditionally fall into three main categories. 
The first category involves informal methods such as software testing and 
monitoring. The second involves formal verification, i.e., model checking and 
theorem proving. The third is abstract interpretation and static program 
analysis techniques.

The goal of this workshop is to promote discussion on novel combinations 
of these methodologies, as well as study the individual contribution of each 
of these methodologies in verifying software. An example of a combined 
verification methodology is the recent research direction that combines 
abstraction (of infinite-state programs into finite-state ones) with model 
checking (of finite-state systems).  There is a growing conviction in the 
research community that such hybrid methodologies are imperative for the 
process of  analyzing full-fledged software systems. This workshop will study 
combination of analysis methodologies for verification of software.  This 
research is very important and timely since

    . Software is being increasingly used to control embedded systems which 
      are often safety critical (such as automobile parts).
    . There is renewed promise in program verification in the recent years 
      due to (a) progress in generating models from code, and 
      (b)  combination of model checking with other analysis techniques such 
      as abstract interpretation.

Topics Covered

The workshop will focus on theoretical techniques, practical methods as well 
as  case studies for verification of  conventional and embedded software 
systems. In particular, we welcome papers which describe combinations of 
formal and informal reasoning, as well as formal verification and program 
analysis techniques. Tool papers and case studies, which report on  advances 
in verifying large scale programs in standard languages are particularly 
sought. The list of topics include, but are not restricted to:

    . Tools, environments and case studies for large scale software 
      verification
    . Static analysis/Abstract interpretation/Program transformations 
      for verification
    . Use of model checking and deductive techniques for software verification
    . Role of declarative programming languages (such as Prolog) for infinite 
      state software verification.
    . Techniques to validate system software (such as compilers) as well as 
      assembly code/Java bytecode
    . Proof techniques for verifying specific classes of software (such as 
      object-oriented programs)
    . Integrating testing and run-time monitoring with formal techniques
    . Validation of UML diagrams, and/or  requirement specifications
    . Software certification and proof carrying code
    . Integration of formal verification into software development projects

Submissions Information

    . Regular submissions should be no more than 15 pages. Short papers (upto 
      5 pages) describing initial ideas are also welcome. All submitted papers 
      should be in PS or PDF. Please avoid using zip, gzip, compress, tar etc. 
      Papers should be submitted via e-mail to zijiang.yang at wmich.edu

    . The workshop proceeding will be published as Electronic Notes in 
      Theoretical Computer Science (ENTCS). Note that ENTCS papers should be 
      at least 10 pages in ENTCS format.

    . The deadlines are as follows.
          . Submission deadline:  September 30, 2005
          . Notification of Acceptance:  October 14, 2005
          . Final Version submission:  October 21, 2005

 Program Committee

    . Rajeev Alur (University of Pennsylvania, USA)
    . Tevfik Bultan (University of California, Santa Barbara, USA)
    . Sandro Etalle (University of Twente, Netherlands)
    . Daniel Kroning (ETH Zurich, Switzerland)
    . Lunjin Lu (Oakland University, USA)
    . C. R. Ramakrishnan (SUNY Stony Brook, USA)
    . Chao Wang  (NEC Laboratories, USA)
    . Farn Wang (National Taiwan University, Taiwan)
    . Yi Wang (Uppsala University, Sweden)
    . Lintao Zhang (Micosoft Research, USA)

Invited Speakers

    . TBA

Organizers

    . Supratik Mukhopadhyay, West Virginia University, USA. 
    . Abhik Roychoudhury, National University of Singapore, Singapore.
    . Zijiang Yang, Western Michigan University, USA (Workshop Co-ordinator).

If you have any queries about the workshop, please send e-mail to 
zijiang.yang at wmich.edu