+\subsection options_modelchecking_visited model-check/visited, Cycle detection
+
+In order to detect cycles, the model-checker needs to check if a new explored
+state is in fact the same state than a previous one. In order to do this,
+the model-checker can take a snapshot of each visited state: this snapshot is
+then used to compare it with subsequent states in the exploration graph.
+
+The \b model-check/visited is the maximum number of states which are stored in
+memory. If the maximum number of snapshotted state is reached some states will
+be removed from the memory and some cycles might be missed.
+
+By default, no state is snapshotted and cycles cannot be detected.
+
+\subsection options_modelchecking_termination model-check/termination, Non termination detection
+
+The \b model-check/termination configuration item can be used to report if a
+non-termination execution path has been found. This is a path with a cycle
+which means that the program might never terminate.
+
+This only works in safety mode.
+
+This options is disabled by default.
+
+\subsection options_modelchecking_dot_output model-check/dot-output, Dot output
+
+If set, the \b model-check/dot-output configuration item is the name of a file
+in which to write a dot file of the path leading the found property (safety or
+liveness violation) as well as the cycle for liveness properties. This dot file
+can then fed to the graphviz dot tool to generate an corresponding graphical
+representation.
+
+\subsection options_modelchecking_max_depth model-check/max_depth, Depth limit
+
+The \b model-checker/max-depth can set the maximum depth of the exploration
+graph of the model-checker. If this limit is reached, a logging message is
+sent and the results might not be exact.
+
+By default, there is not depth limit.
+
+\subsection options_modelchecking_timeout Handling of timeout
+
+By default, the model-checker does not handle timeout conditions: the `wait`
+operations never time out. With the \b model-check/timeout configuration item
+set to \b yes, the model-checker will explore timeouts of `wait` operations.
+
+\subsection options_modelchecking_comm_determinism Communication determinism
+
+The \b model-check/communications-determinism and
+\b model-check/send-determinism items can be used to select the communication
+determinism mode of the model-checker which checks determinism properties of
+the communications of an application.
+
+\subsection options_modelchecking_sparse_checkpoint Per page checkpoints
+
+When the model-checker is configured to take a snapshot of each explored state
+(with the \b model-checker/visited item), the memory consumption can rapidly
+reach GiB ou Tib of memory. However, for many workloads, the memory does not
+change much between different snapshots and taking a complete copy of each
+snapshot is a waste of memory.
+
+The \b model-check/sparse-checkpoint option item can be set to \b yes in order
+to avoid making a complete copy of each snapshot: instead, each snapshot will be
+decomposed in blocks which will be stored separately.
+If multiple snapshots share the same block (or if the same block
+is used in the same snapshot), the same copy of the block will be shared leading
+to a reduction of the memory footprint.
+
+For many applications, this option considerably reduces the memory consumption.
+In somes cases, the model-checker might be slightly slower because of the time
+taken to manage the metadata about the blocks. In other cases however, this
+snapshotting strategy will be much faster by reducing the cache consumption.
+When the memory consumption is important, by avoiding to hit the swap or
+reducing the swap usage, this option might be much faster than the basic
+snapshotting strategy.
+
+This option is currently disabled by default.