Image courtesy of Royal Society
Fourth International Workshop on Automated Verification of Critical Systems : AVoCS'04
4 September 2004 London (UK)
Affiliated with Concur 2004
Scope Topics Call for Papers Instructions to Authors Proceedings Important Dates Keynote Speaker Programme Contact & Registration Fees Venue & Travel Pictures Accommodation London Travel Info Programme Committee Sponsors & Supporters Previous Events: AVoCS'01AVoCS'02 AVoCS'03


The aim of this workshop is to promote a research community in verification of critical systems through encouraging communication among researchers. Specific objectives include efforts at integration as well as the transfer of methods between different groups from academia and industry. The topics are to be interpreted broadly and inclusively, and in particular cover all aspects of verification (model checking, theorem proving, specification and refinement proofs, etc) pertaining to various types of critical systems, be it safety-critical, business-critical, or performance-critical.

The first meeting, AVoCS'01, was held in Oxford (UK), continuing in the tradition of the annual DERA/OUCL series. The second meeting, AVoCS'02, was held in Birmingham (UK). The third meeting, AVoCS'03, was held in Southampton (UK) and was international in scope. Similarly to previous years, the meeting will be informal, and will combine an invited lecture with accepted submissions. This year we run this event as a fully-fledged international workshop.


Topics include but are not limited to:
  • Specification and Refinement Methods
  • Requirements Capture and Analysis
  • Model checking : Theory, Tools and Applications
  • Abstract Interpretation
  • Theorem Proving
  • Software and Hardware Verification
  • Verification of Probabilistic and/or Real-Time Systems
  • Verification of Distributed Protocols including Security
  • Performance and Dependability Evaluation
  • Case Studies

and should apply to, or have relevance for, critical systems in a broad sense.

Call for Papers

Download self-contained call for papers in text format.

Instructions to Authors

Please click here for instructions for the preparation of the final online ENTCS proceedings.

Please submit an abstract or extended abstract in PDF format and a plain-text abstract electronically to M.Huth "at" Submissions should not exceed 15 pages, including references, and should be written in Latex using the ENTCS templates found at . You should follow the instructions on the ENTCS Macro Home Page, being sure to pull off the appropriate file for the AVoCS'04 workshop. Abstracts may be as short as two pages. Only abstracts and papers accepted for presentation at the workshop will be included in the Preliminary Proceedings. 


Proceedings will be published in the series Electronic Notes in Theoretical Computer Science, now widely disseminated through Science Direct. Preliminary proceedings of accepted papers should be available as hard-copies at the workshop. Final online proceedings of accepted and revised papers will be available after the workshop. We also plan a special issue of a high-quality journal for which we will solicit abstracts of proposed full papers from all workshop participants subsequent to the meeting.

Important Dates

Deadline for Submissions: 9 June 2004 - 17:00 GMT.
Notification of Acceptance: 9 July 2004 - 17:00 BST.
Deadline for Early Registration: 30 July  2004
Workshop Date: 4 September  2004.
Deadline for camera-ready papers for prelimiary proceedings: 9 August 2004 - 17:00 BST.
Deadline for submission of full paper for final proceedings and a special issue: TBA.

Keynote Speaker

Georges Gonthier. Microsoft Research (Cambridge, UK): Extracting Algorithms from Code.




Please consult the Concur 2004 web site about fees for workshops affiliated with Concur 2004.

Contact & Registration

You will have to register through the Concur 2004 registration mechanism.
For all other communication concerning AVoCS'04, including submissions, please send e-mail to M.Huth "at"

Venue & Travel & Dinner

The Royal Society, 6-9 Carlton House Terrace, London, SW1Y 5AG. Click here for travel directions and for a map of the Royal Society Building and its surrounding area. Please be advised that the District Line won't run on 4 September due to engineering work. If talks don't run over time, we can have an informal wrap-up discussion between 17:30 and 18:00 but we have to vacate the building at 18:00.


courtesy of Pierre Yves Schobbens


Participants are kindly asked to book their own accommodation. Here is a list of low to moderate cost hotels and guest houses. Please also see the local arrangements of Concur 2004 for further accommodation information. For more exclusive accommodations please click here.

Local Organisers

Michael Huth and Sebastian Uchitel, Imperial College London


Programme Committee

Glenn Bruns, Bell Laboratories, Lucent Technologies (USA)
Michael Goldsmith, Formal Systems (Europe) Ltd (UK)
Michael Huth, Imperial College London (UK)
Marta Kwiatkowska, University of Birmingham (UK)
Michael Leuschel, University of Southampton (UK)
David Nowak, CNRS & ENS Cachan (FR)
Doron Peled, University of Warwick (UK)
Bill Roscoe, Oxford University (UK)

Sponsors & Supporters