MARS 2027

Submission timeline

• 22 Jan 2027 Full paper AoE
• 5 Mar 2027 Notification

• 11 Apr 2027 Conference opens

What to submit

Format

15 pages EPTCS + references

Proceedings

EPTCS — CC BY-SA

Chairs and
invited speakers

Only men

chairs 1 man, 0 womeninvited speakers 2 men, 0 women

How this is counted

Co-located with

TACAS 2027
Satellite of ETAPS.

In addition to the workshop proceedings, the formal models presented at the workshop will be archived in the MARS Repository.

Call for papers

• As first published MARS-2027.txt · TXT · shown below

The call, as published

Reproduced verbatim from the organisers’ announcement. The conference’s own page is at mars-workshop.org/mars2027/.

                            Call for Papers

               Models for Formal Analysis of Real Systems
                              (MARS 2027)

                            April 11, 2027
                         Copenhagen, Denmark
                      Affiliated with ETAPS 2027

                  https://mars-workshop.org/mars2027/


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 distributed and decentralised
systems, cyber-physical systems, hardware/software codesign, biology,
finance, quantum and reversible computing, etc.
The motivation and aim for MARS stem from the following two observations:

  * Large case studies are essential to show that specification formalisms
    and modelling techniques are applicable to real systems, whereas many
    research papers only consider toy examples or tiny case studies.
  * Developing an accurate model of a real system takes a large amount of
    time, often months or years. In most scientific papers, however,
    salient details of the model need to be skipped due to lack of space
    as well as to leave room for formal verification methodologies and
results.

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:

  * Which formalism was chosen, and why?
  * Which abstractions have been made, and why?
  * How were important characteristics of the system modelled?
  * Were there any complications while modelling the system?
  * Which measures were taken to guarantee the accuracy of the model?
  * How can different modelling approaches be compared on this system?

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.

SUBMISSION GUIDELINES

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 under review
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 2027 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 uploaded in PDF format via
EasyChair (https://easychair.org/conferences/?conf=mars2027).
Contributions are limited to 15 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 with accepted papers will be made
available in the MARS Repository. A URL to the formal models should be
provided along with the submission.

IMPORTANT DATES (AoE)

  * Submission: Friday, January 22, 2027
  * Notification: Friday, March 5, 2027
  * Final version: Wednesday, March 24, 2027
  * Workshop: Sunday, April 11, 2027

KEYNOTES

Alessandro Cimatti (Fondazione Bruno Kessler, Italy)
Jan Friso Groote (TU Eindhoven, Netherlands)

PROGRAM COMMITTEE

Marco Bernardo (University of Urbino, Italy, chair)
Jane Hillston (University of Edinburgh, United Kingdom)
Radu Mateescu (INRIA Center at Université Grenoble Alpes, France)
David Parker (University of Oxford, United Kingdom)
Tatjana Petrov (University of Trieste, Italy)
Anna Philippou (University of Cyprus, Cyprus)
Anne Remke (University of Münster, Germany)
Christian Schilling (Aalborg University, Denmark)
Marjan Sirjani (Mälardalen University, Sweden)
Maurice ter Beek (CNR-ISTI, Italy)
Matthias Volk (TU Eindhoven, Netherlands)

VENUE AND TRAVEL INFORMATION

MARS 2027 is part of the European Joint Conferences on Theory and
Practice of Software (ETAPS 2027). Information about the venue and
travelling in/to Denmark can be found on the web page of ETAPS.

WORKSHOP ORGANISERS AND CONTACT

All questions about the workshop should be emailed to Marco Bernardo
and Christian Schilling via mars2027@mars-workshop.org

SUPPORT

MARS 2027 benefits from the financial support by the Interreg North
Sea project "Software reliability for critical infrastructures"
(STORM_SAFE; https://www.interregnorthsea.eu/stormsafe).