We give an overview on our approach to symbolic simulation
in the PVStheorem prover and to demonstrate its usage in the realm
of validation by executing specification on incomplete data. In this way,
one can test executable models for a possibly infinite class of test vectors
with one run only. One of the main benefits of symbolic simulation in a
theorem proving environment is enhanced productivity by early detection
of errors and increased confidence in the specification itself.