First International Workshop on Automated Verification of Infinite-State Systems (AVIS'01) 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; precise details to be confirmed. 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. Important Dates 19th January 2001 Submission of abstracts 2nd February 2001 Notification of acceptance 16th February 2001 Camera-ready copies due 12th March 2001 Workshop 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 which will be available at the workshop. Authors of selected papers may be invited to submit full and revised papers for a special journal issue after presentation at the workshop. Lecturer's Biography Dr. Ramesh Bharadwaj holds the BE, ME, and PhD degrees in Electrical and Computer Engineering. His industrial experience includes several years of software and hardware development, and software project management. He has held research and development positions at several industrial and research organizations, including Philips Research Laboratories, the Tata Institute of Fundamental Research, Stanford University, Communications Research Laboratory, and AT&T Bell Laboratories. He is currently a researcher in Software Engineering at the Naval Research Laboratory. His research interests include methods and tools for formal requirements specification, analysis, and verification, automatic theorem proving, abstraction, model checking, and decision procedures.