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).

List of all models

Description Formalism(s) Event
Robotic Cell Injection Discrete-Time Markov Chain (PRISM) MARS'17
Production Cell LNT (CADP); LOTOS (CADP) MARS'17
A Model-Derivation Framework for Software Analysis Uppaal MARS'17
Emergency Power Supply BDMP(KB3) MARS'17
AUTOSAR Erlang QuickCheck MARS'17
Message Authenticator Algorithm REC tool; AProVE tool; Clean; Haskell; LNT (CADP); LOTOS (CADP); Maude; mCRL2; OCaml; Opal; Rascal; Scala; Standard ML; Stratego/XT; Tom MARS'17
IEEE 802.15.4 TCSH MAC mCRL2 tool suite MARS'17
Memory Access and Interrupts Isabelle/HOL MARS'17
B.A.T.M.A.N. Uppaal MARS'17
Fragmentation and Reassembly for CAN AWN MARS'17
Stream Control Transmission Protocol Uppaal MARS'17
Bitcoin Protocol Uppaal MARS'15
Caches and Pipelines Uppaal MARS'15
Self-Balancing Unicycles SpaceEx; Mathematica MARS'15
eChronos Isabelle/HOL MARS'15
Bilby File System Isabelle/HOL MARS'15

All models are licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.

© 2015-17, Last Update April 18, 2017.