International Workshop on Software Verification and Validation (SVV 2005)

In Conjunction with
International Conf. on Formal Engg. Methods (ICFEM) 2005

Manchester UK, October 31 2005

• Goal of the Workshop
• Workshop Schedule with Accepted Papers  (NEW)
  
• Topics Covered
• Submissions Information
• Program Committee
• Invited Speakers
• Organizers
• Past SVV Workshops

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.

• 0830-0930 Registration
• 0930-1015 Abstract Graph Transformation --  Arend Rensink, Dino Distefano
• 1015-1100 A model checking-based tool for verification of web applications --  Marina Mongiello, Daniela Castelluccia, Rodolfo Totaro, Michele Ruta
• 1100-1130 Coffee break
• 1130-1215 A Z Approach in Validating ORA-SS Data Models --  Scott Lee, Jing Sun, Gillian Dobbie, Yuan Fang Li
• 1215-1400 Lunch
• 1400-1445 Parallel Assignments in Software Model Checking -- Murray Stokely, Sagar Chaki, Joel Ouaknine
• 1445-1530 A Semiring-based Quantitative Analysis of Mobile Systems -- Benjamin Aziz
• 1530-1600 Coffee break
• 1600-1645 Model Checking Temporal Aspects of Inconsistent Concurrent Systems Based on Paraconsistent Logic -- Donghuo Chen, Jinzhao Wu
• 1645-1730 Invited talk by Farn Wang
• 1730          Close
  
  

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@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:  October 4, 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

• Dr. Farn Wang, Department of Electrical Engineering, National Taiwan University 

• TITLE: Automatic Test Case Generation with Region-Related Coverage Annotations for
  Real-time Systems 

• Abstract: Testing is the mainstream of verification techniques used for real-time systems in the industry because it allows the engineers to directly observe how their system implementations react to various test cases. In this paper, we investigate how to use symbolic techniques to automatically generate test cases for real-time systems. Especially, our test cases have two annotations that can be useful in the construction of powerful test cases. First, events in our test cases are labeled with symbolic timing constraints which can either be conveniently used in picking event occurrence times or be used for choosing boundary timing values in domain analysis. Second, our test cases are annotated with region-related coverage estimations which support high precision in detecting some timing bugs. Finally, we have implemented our ideas with BDD-like data-structures which could lead to performance advantage for testing complex embedded systems.

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@wmich.edu

Past  SVV Workshops

• SVV 2003,December 14, 2003, Venue: Mumbai (India).
• SVV 2004,November 8, 2004, Venue: Seattle, (USA).