Program new!

Program Committee

                   Ramesh Bharadwaj               (Program Chair) Naval Research Laboratory, USA
                   Michael Colon                        Naval Research Laboratory, USA
                   Javier Esparza                         University of Stuttgart, D
                   Ralph Jeffords                         Naval Research Laboratory, USA
                   Supratik Mukhopadhyay      West Virginia University, USA
                   Joel Ouaknine                         Carnegie Mellon University, USA
                   R. Ramanujam                        The Institute of Mathematical Sciences, IND
                    Wolfgang Reif                         Universität Augsburg, D
                   Tomas Uribe                            SRI International, USA

Invited Speakers

Thomas Ball Microsoft Research, USA

Patrick Cousot Ecole Normale Superieure, FR

Cathy Meadows Naval Research Laboratory, USA

Thomas Reps University of Wisconsin, USA

Scott Stoller SUNY at Stony Brook, USA

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.

The Workshop

The workshop will be co-located with European Joint Conferences on Theory and Practice of Software 2004 March 27-April 4, Barcelona, Spain. The two day workshop will be held on 3rd and 4th April 2004.

Submission

You are invited to submit a full paper, 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.
You are required to submit an abstract prior to your paper submission.

Abstract submissions are to be sent to AVIS04abs@itd.nrl.navy.mil and
paper submissions to AVIS04sub@itd.nrl.navy.mil.

Important Dates

19th December 2003 Submission of abstract

05th January 2004 Submission of full paper

06th February 2004 Notification of acceptance <-- Note revised date

23rd February 2004 Camera-ready copies due

3rd-4th April 2004 Workshop

Workshop Organizers

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

Publication

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. Authors: please refer to the ENTCS web site for formatting instructions and use the prentcsmacro.sty for AVIS.

The appearance of external hyperlinks does not constitute endorsement by the United States Department of Defense, the United States Department of the Navy and The Naval Research Laboratory of the linked web sites, or the information, products or services contained therein. For other than authorized activities such as military exchanges and Morale, Welfare and Recreation (MWR) sites, the United States Department of Defense, the Department of the Navy and The Naval Research Laboratory does not exercise any editorial control over the information you may find at these locations. Such links are provided consistent with the stated purpose of this DoD web site.

This Is An Official U.S. Navy Web Site

Privacy Policy

Created: Ramesh Bharadwaj | Updated: 23rd March 2004

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