Affiliated with the
European Joint Conferences on Theory and Practice of Software (ETAPS 2022)
The MARS workshops bring together researchers from different communities who are developing formal models of real systems in areas where complex models occur, such as networks, cyber-physical systems, hardware/software codesign, biology, etc. The motivation and aim for MARS stem from the following two observations:
The MARS workshops aim at remedying these issues, emphasising modelling over verification, so as to retain lessons learnt from formal modelling, which are not usually discussed elsewhere. Examples are:
We thus invite papers that present formal models of real systems, which may lay the basis for future analysis and comparison.
In addition to the workshop proceedings, the formal models presented at the workshop will be archived in the MARS Repository, a growing, diverse collection of realistic benchmarks. The existence of this repository is a unique feature that makes MARS contributions available to the wider community, so that others can reproduce experiments, perform further analyses, and try the same case studies using different formal methods.
|Registration and Opening
Invited Talk I
Modeling the Raft Distributed Consensus Protocol in LNT (MARS'20)
Formal Quantitative Modeling
Stateful to Stateless: Modelling Stateless Ethereum (MARS'22)
Sandra Johnson, David Hyland-Wood, Anders Madsen, and Kerrie Mengersen
Modeling an Asynchronous Circuit Dedicated to the Protection Against Physical Attacks (MARS'20)
Radu Mateescu, Wendelin Serwe, Aymane Bouzafour, and Marc Renaudin
Formally Modeling Autonomous Vehicles in LNT for Simulation and Testing (MARS'22)
Lina Marsso, Radu Mateescu, Lucie Muller, and Wendelin Serwe
Formal Modelling and Initial Analysis of the 4SECURail Case Study (MARS'22)
Franco Mazzanti and Dimitri Belli
Invited Talk II
Modest Models and Tools for Real Stochastic Timed Systems (MARS'22)
Protocol and Controller Modeling
Formalising the Optimised Link State Routing Protocol (MARS'20)
Ryan Barry, Rob van Glabbeek, and Peter Höfner
Iterative Variable Reordering: Taming Huge System Families (MARS'20)
Clemens Dubslaff, Andrey Morozov, Christel Baier, and Klaus Janschek
Advanced Models for the OSPF Routing Protocol (MARS'20/22)
Courtney Darville, Peter Höfner, Franc Ivankovic, and Adam Pam
Modeling R3 Needle Steering in Uppaal (MARS'20/22)
Sascha Lehmann, Antje Rogalla, Maximilian Neidhardt, Anton Reinecke, Alexander Schlaefer, and Sibylle Schupp
All submissions will be peer-reviewed by at least three referees based on their novelty, relevance, and technical merit. The MARS proceedings will be published in the open-access EPTCS series (Electronic Proceedings in Theoretical Computer Science).
Submissions must be unpublished and not be submitted for publication elsewhere. It is accepted, however, to submit a paper about a case study already mentioned at another conference, workshop, or journal provided that: (1) the formal model is submitted to MARS 2022 and has not been published previously, and (2) the MARS submission adds significant, novel material concerning the formal modelling work.
Submissions must be in English and submitted in PDF format via EasyChair. Contributions are limited to 12 pages EPTCS style (not counting references and the appendices). Appendices (of arbitrary length, included in the proceedings) can be added to present all details of a formal model.
We welcome submissions that come together with one or many formal models that can be processed by some tool (e.g., timed automata for Uppaal, definitions and proofs for Isabelle/HOL, etc.). Such models should be complete (i.e., self-contained) and made available under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License. The models associated to accepted papers will be made available in the MARS Repository. A URL to the formal models should be provided along with the submission.
|Monday, 28 February 2022
MARS 2022 is part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2022). Information about venue and travelling in/to Munich can be found at the webpage of ETAPS. As the main conference, the workshop is planned as an on-site event but with some degree of support for online attendance.
All questions about the workshop should be emailed to the PC chairs Clemens Dubslaff and Bas Luttik at email@example.com