Fourth International Workshop on
Automated Verification of Infinite-State Systems (AVIS'05)
Co-located with ETAPS 2005

2nd - 3rd April 2005
Edinburgh, Scotland

Program Committee

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
John Goodenough Software Engineering Institute, CMU, USA
Ralph Jeffords      Naval Research Laboratory, USA
Supratik Mukhopadhyay (Program Co-Chair) West Virginia University, USA
Abhik Roychoudhury     National University of Singapore, SG
Stefan Schwoon  University of Stuttgart, D
Sandeep Kumar Shukla   Virginia Tech, USA

Invited Speakers              

Dr. Rustan Leino   Microsoft Research, USA                                                        
Prof. Bernhard Steffen  University of Dortmund, D
Dr. Carolyn Talcott   SRI International, USA

Program new!


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 2005 2-10 April 2005, in Edinburgh, Scotland.   The two day workshop will be held on 2nd and 3rd April 2005.
 

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 AVIS05abs@itd.nrl.navy.mil and paper submissions to AVIS05sub@itd.nrl.navy.mil.
 

Important Dates                    NOTE: REVISED DATES!

  •    7th     January  2005   Submission of abstract
  •   24th     January  2005   Submission of full paper
  •    7th     February 2005   Notification of acceptance
  •   25th     February 2005   Camera-ready copies due
  •   2nd-3rd  April    2005   Workshop

    •  

    Workshop Organizers

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

    Dr. Supratik Mukhopadhyay
    Department of Computer Science
    West Virginia University
    Morgantown, WV 26506-6109  USA
     

    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: 21st March 2005