Verification Modulo Theories was originally proposed in the Rich-Model Toolkit meeting held in Turin in 2011 (see slides below).
Since then, a format has been defined (see below), and is now supported by the the nuXmv model checker.
The VMT format is an extension of the SMT-LIBv2 (SMT2 for short) format to represent symbolic transition systems. VMT exploits the capability offered by the SMT2 language of attaching annotations to terms and formulas in order to specify the components of the transition system and the properties to verify.
In the core VMT-LIB language, the following annotations are used:
:next name is used to represent state variables. For each variable x in the model, the VMT file contains a pair of variables, xc and xn, representing respectively the current and next version of x. The two variables are linked by annotating xc with the attribute :next xn. All the variables that are not in relation with another by means of a :next attribute are considered inputs.
:init is used to specify the formula for the initial states of the model. This formula should contain neither next-state variables nor input variables.
:trans is used to specify the formula for the transition relation.
:invar-property idx is used to specify invariant properties, i.e. formulas of the form Gp, where p is the formula annotated with :invar-property. The non-negative integer idx is a unique identifier for the property.
:live-property idx is used to specify an LTL property of the form F Gp, where p is the formula annotated with :live-property. The non-negative integer idx is a unique identifier for the property.
In a VMT file, only annotated terms and their sub-terms are meaningful. Any other term is ignored. Moreover, only the following commands are allowed to occur in VMT files: set-logic, set-option, declare-sort, define-sort, declare-fun, define-fun (For convenience, an additional (assert true) command is allowed to appear at the end of the file).
The following example shows a simple NUXMV model and its corresponding VMT translation.