AVIS'04 Call for Papers

[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

Prolog: Topics of the workshop include static analysis of programs.

                         CALL FOR PAPERS
                  Third International Workshop on
        Automated Verification of Infinite-State Systems (AVIS'04)
                      Co-located with ETAPS 2004

                         28th March 2004
                         Barcelona, Spain

This workshop 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

You are invited to submit an extended abstract, not to exceed 10 pages, on
related research or case study.  We invite both completed work as well as
work in progress; the aim of the workshop is to stimulate discussion and
to bring together people with varying backgrounds from disparate

Important Dates
#   19th December 2003   Submission of extended abstract
#   05th January  2004   Submission of paper
#   16th January  2004   Notification of acceptance
#   23rd February 2004   Camera-ready copies due
#   28th March    2004   Workshop

The accepted papers will be published in the proceedings which will be
available at the workshop.  The proceedings will also be published
electronically on ENTCS.

Program Committee
Ramesh Bharadwaj   (Program Chair) Naval Research Laboratory USA
Michael Colon  Naval Research Laboratory USA
Javier Esparza  University of Stuttgart (D)
Supratik Mukhopadhyay   NASA/WVU Software Research Lab  USA
Joel Ouaknine   Carnegie Mellon University USA
R. Ramanujam  The Institute of Mathematical Sciences  IND
Wolfgang Reif   University of  Augsburg (D)

The website for the workshop is: