  There is a growing interest in modeling and analyzing the spread of diseases
like the SARS-CoV-2 infection using stochastic models. These models are
typically analyzed quantitatively and are not often subject to validation using
formal verification approaches, nor leverage policy syntheses and analysis
techniques developed in formal verification. In this paper, we take a Markovian
stochastic model for the spread of a SARSCoV-2-like infection. A state of this
model represents the number of subjects in different health conditions. The
considered model considers the different parameters that may have an impact on
the spread of the disease and exposes the various decision variables that can
be used to control it. We show that the modeling of the problem within
state-of-the-art model checkers is feasible and it opens several opportunities.
However, there are severe limitations due to i) the espressivity of the
existing stochastic model checkers on one side, and ii) the size of the
resulting Markovian model even for small population sizes.
