In this work we present an Eclipse plug-in for the VInTiMe (Verifier of INtegrated TImed ModEls)1 suite of tools that combines high-level expressive power, unassisted propertypreserving model reduction and distributed model checking to describe and verify complex real-time system designs and their properties. Keywords Eclipse plug-in, timed model checking, verification, timed automata, Lapsus, ObsSlice, VTS, Zeus