# TMV

TMV is a model checker for timed systems, e.g., timed automata, which have real-valued clocks or timer variables
in addition to Boolean state variables. It is *fully symbolic*, meaning
that it uses a single symbolic representation for both Boolean and real-valued parts of the state space; this
representation is a formula in *separation logic* (also called *difference logic*). A formula in separation logic is
a Boolean combination of Boolean variables and two-variable linear constraints
called separation or difference-bound constraints (e.g., *x* > *y* + 3).
The image computation step involves eliminating quantifiers from a formula in *quantified separation logic* (QSL).
The key theoretical contribution in TMV is a translation of a QSL formula to an equivalent quantified Boolean
formula (QBF). Standard Boolean quantifier elimination techniques can be
used on the resulting QBF.
The translation of QSL to QBF incorporates some optimizations specific to timed model checking.

Here is a paper which describes the translation of QSL to QBF and a model checker for timed automata.

**
Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean
Methods.
**
Sanjit A. Seshia and Randal E. Bryant.
* In Proc. Intl. Conf. on Computer-Aided
Verification (CAV), LNCS 2725, pages 154-166, July 2003.
*
A more detailed version of this paper, with proofs, is available as a technical report.

**
A Boolean Approach to Unbounded, Fully Symbolic Model Checking of Timed Automata.
**
S. A. Seshia and R. E. Bryant.
*Computer Science Department Technical report CMU-CS-03-117, March 2003.*
TMV has been successfully applied to the verification of timed circuits. Here
is a paper describing a novel modeling methodology and applications of TMV
to industrial circuits.

**
Modeling and Verifying Circuits Using Generalized Relative Timing.
**
Sanjit A. Seshia, Randal E. Bryant, and Kenneth S. Stevens.
*
11th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC),
March 2005, pages 98-108.
*