| Ramesh Bharadwaj | (Program Co-Chair) Naval Research Laboratory, USA |
| Tevfik Bultan | University of California, Santa Barbara, USA |
| Supratik Chakraborty | Indian Institute of Technology Bombay, IND |
| Michael Colón | Naval Research Laboratory, USA |
| Ralph Jeffords | Naval Research Laboratory, USA |
| Supratik Mukhopadhyay | (Program Co-Chair) West Virginia University, USA |
| Sandeep Kumar Shukla | Virginia Tech, USA |
| TBD |
This workshop builds upon the successes of AVIS'01, AVIS'03,
AVIS'04, and AVIS'05 which were held respectively in Berlin, Germany in
conjunction with Formal Methods Europe 2001 (FME-01); in Warsaw, Poland
in conjunction with ETAPS 2003; in Barcelona, Spain, in conjunction
with ETAPS 2004, and in Edinburgh, UK in conjunction with ETAPS
2005. It is a forum for researchers, students, and practitioners
interested in the application of formal methods and tools for the
automatic verification of large practical systems. Formal
methods, in particular model checking, is increasingly being used in
industry to automatically establish the correctness of (and to find
flaws in) finite-state systems, such as descriptions of hardware and
protocols. However, model checking is limited in scope due to the
state explosion problem. Most practical system descriptions,
notably that of software, are therefore not directly amenable to
finite-state verification methods since they have very large or
infinite state spaces. For such systems, theorem proving - a
process that requires manual effort and mathematical sophistication to
use - has so far been the only viable alternative.
More recently, we have seen the emergence of hybrid techniques that
combine the ease-of-use of model checkers with the power of theorem
provers.
Tools based on these techniques afford users with full automation, and
are less sensitive to the size of the state space (which may be
infinite
or arbitrarily large). There is a growing body of knowledge in
this
field which has a very exciting future. The intention of this workshop
is to build a forum for exchanging ideas and experiences by bringing
together
theoreticians, tool builders, as well as practitioners who are
interested
in this emerging area of research in formal verification.
Formal verification is poised to play a key role in the design,
analysis, and certification of mission-critical systems. However,
techniques such as model checking do not scale to practical systems,
especially to systems that have software as their major components.
What is needed are new paradigms and methods that combine the ease of
use of model checking with the power and flexibility of theorem
proving. Such methods do scale, especially to software-intensive
systems, as exemplified by a number of Industrial case studies.
The AVIS series of workshops is intended as a forum to bring together
researchers from diverse areas such as model checking, formal methods,
abstract interpretation, decision procedures, automatic invariant
generation, proof systems, theorem proving systems, etc., to exchange
ideas and build a forum that would not only be useful to practitioners
but also further the state-of-the-art in verification technology.
ETAPS is a forum for academic and industrial researchers working on
topics related to software science. In particular, the TACAS
series concentrates on tools for the construction and analysis of
systems. AVIS complements the conferences very nicely by
providing researchers a forum for the exchange of early research
results, and for furthering the state-of-the-art in the verification of
large practical systems, including software-intensive systems.
Dr. Supratik Mukhopadhyay
Department of Computer Science
West Virginia University
Morgantown, WV 26506-6109 USA
This Is An Official U.S. Navy Web Site