AVIS'01: LAST Call for Abstracts

[Ramesh Bharadwaj]

                      First International Workshop on
          Automated Verification of Infinite-State Systems (AVIS'01)
      http://www.informatik.hu-berlin.de/top/fme2001/html/workshops.html

                Co-located with FME 2001 in Berlin, Germany
                            12th March 2001


This workshop is a forum for researchers, students, and practitioners
interested in the application of formal methods and tools for the auomatic
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.


The Workshop

The workshop will be co-located with FORMAL METHODS EUROPE 2001
"Formal Methods for Increasing Software Productivity" 12-16 March 2001,
Humboldt-Uinversitaet zu Berlin, Germany.  The workshop will be held on
12th March.


Submission

You are invited to submit a 2-4 page abstract 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 bring together
people with varying backgrounds from disparate communities.

Submission should be made electronically to

    ramesh@itd.nrl.navy.mil

We accept plain text, pdf, or postscript submissions.

Authors of accepted abstracts will be expected to give a 20 minute
presentation at the workshop.

Important Dates

  16th February 2001  Submission of abstracts
  2nd  March    2001  Notification of acceptance
  12th March    2001  Workshop
  15th June     2001  Camera-ready copies due


Workshop Organizers

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

Dr. Steve Sims
Chief Technology Officer -- Reactive Systems, Inc.
http://www.reactive-systems.com
sims@reactive-systems.com
+1-703-534-6458

Publication

The accepted papers will be published as a Naval Research Laboratory
Technical Memorandum.  Authors of selected papers may be invited to
submit full and revised papers for a special journal issue after
presentation at the workshop.