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.