12 April 2003, Second International Workshop on Automatic Analysis of Infinite-State Systems (AVIS'03)

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 verification.

AVIS'03 will be co-located with the European Joint Conference on Theory and Practice of Software 2003 April 5-13, Warsaw, Poland (see http://www.mimuw.edu.pl/etaps03/). The workshop will be held on 12th April 2003.

Submission

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 communities.

The accepted papers will be published in the proceedings which will be available at the workshop. As with AVIS'01, authors of selected papers will be invited to submit full and revised papers for a special journal issue after presentation at the workshop.

Important Dates

04th January 2003 Submission of extended abstract
16th February 2003 Notification of acceptance
28th February 2003 Camera-ready copies due
12th April 2003 Workshop

Workshop Organizer

Dr. Ramesh Bharadwaj
Center for High Assurance Computer Systems
Naval Research Laboratory
Washington DC 20375 USA
ramesh at itd.nrl.navy.mil
+1-202-767-7210

For more information, visit http://chacs.nrl.navy.mil/AVIS03/.