Modelling techniques, aiming at the accurate description of systems and their relevant properties, are typically developed with formal analysis and formal verification in mind. To show that a developed approach actually scales to real systems, large case studies are essential.
To share insight and information concerning the development of models we regularly run workshops on Models for formal Analysis of Real Systems (MARS). They focus the modelling effort itself, rather than the subsequent analysis and verification.
This webpage provides not only links to the workshops, it also presents all models presented at the workshops. The models come free of charge and we encourage everybody to use them. New models and adapted versions of existing models (e.g. same model in a different formalism) are most welcome. Please send your submission to

photograph coutesy NASA


The workshop aims at discussing lessons learnt while creating large models. Examples are:
  • Which formalism is chosen, and why?
  • Which abstractions have to be made and why?
  • How are characteristics of the system modelled?
  • Were there any complications while modelling?
  • How is the accuracy of the model measured?
The workshops emphasise modelling over verification. In particular, we usually invite papers that may lay the basis for future formal analysis. The workshops bring together researchers from different communities that all aim at verifying real systems and are developing formal models for such systems.
photograph coutesy NASA


The process of developing a detailed and accurate model usually takes a large amount of time, often months or years; without even starting a formal analysis. When publishing the results on a formal analysis in a scientific paper, details of the model have to be skipped due to lack of space.
The models presented during the MARS workshops are made available on a perennial form, so that they can be used by others and that the experiments are reproducible. The list of models is expected to grow as time passes, and to be as diverse as possible. The repository of models is hosted by Inria (France).