International Workshop on Software Verification and Validation (SVV 2003)
In Conjunction with
International Conf. on Logic Programming (ICLP) 2003
Mumbai (India), December 14 2003
Session 1 : Invited Talk and Best Paper Presentation
09:00 - 10:00 Rigorous Methods for Software Construction: Retrofitting "Engineering" into Software Engineering
Invited Talk by Ramesh Bharadwaj (Naval Research Labs, USA)
10:00 - 10:30 Provably Correct Code Generation: A Case Study [Abstract]
Qian Wang and Gopal Gupta (Univ. of Texas at Dallas, USA)
Session 2 : Verification and Static Analysis
11:00 - 11:30 A Denotational Approach to Static Analysis of Cryptographic Processes [Abstract]
Benjamin Aziz, G.W. Hamilton and D. Gray (Dublin City University, Ireland)
11:30 - 12:00 Verifying a UMTS protocol using SPIN and EASN [Abstract]
M. Luukkainen, Vivek K. Shanbhag and K. Gopinath
(University of Helsinki, Finland and Indian Institute of Science)
12:00 - 12:30 Insights to Angluin's Learning [Abstract]
Therese Berg, Bengt Jonsson, Martin
Leucker, Mayank Saksena (Uppsala Univ, Sweden)
12:30 - 13:00 A Trace Logic for Local Security Properties [Abstract]
Ricardo Corin, Antonio Durante, Sandro Etalle and Pieter Hartel
(Univ. of Twente, Netherlands and Universita di Roma, Italy)
Session 3: Formal Specification
14:00 - 14:30 Verification of Scenario-based Specifications using Templates [Abstract]
Girish Palshikar and Purandar Bhaduri (Tata Research Development and Design Centre, India)
14:30 - 15:00 Logical Spec. and Analysis of Fault Tolerant Systems Through Partial Model Checking [Abstract]
S. Gnesi, G. Lenzini and F. Martinelli (C.N.R., Italy)
15:00 - 15:30 Equational Abstractions for Model Checking Erlang Programs [Abstract]
Thomas Noll (Aachen University, Germany)
15:30 - 16:00 Compositional Properties of Sequential Processes [Abstract]
Naijun Zhan (Mannheim Universitat, Germany)
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
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:
The one day workshop will mostly involve talks of peer reviewed research papers in an informal setting. We plan to have several break-out sessions apart from the research paper sessions to promote informal discussions.
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 svv03@comp.nus.edu.sg
We will publish selected papers from the workshop 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.
If you have any queries about the workshop, please send e-mail to abhik@comp.nus.edu.sg