Advances in Computing Science.
From Tool Support for System Specification, Development and Verification.
Edited by Rudolph Bergahmmer and Yassine Lakhnech.
Springer-Verlag, Malente, Germany.
June, 1998.
Pages 189–200.

We give an overview on our approach to symbolic simulation in the PVS theorem prover and 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.

@article{unspecified,
    AUTHOR = {Stephan Pfab and Harald Rue\ss and Sam Owre and and Friedrich {W.} von Henke},
    TITLE = {Towards Light-Weight Verication and Heavy-Weight Testing},
    YEAR = {1998},
    PAGES = {189--200},
    MONTH = {jun},
    NOTE = {Proceedings published in May 1999},
    ADDRESS = {Malente, Germany},
    URL = {http://www.csl.sri.com/papers/fmtools99/},
    SERIES = {Advances in Computing Science},
    BOOKTITLE = {Tool Support for System Specification, Development and Verification},
    PUBLISHER = {Springer-Verlag},
    EDITOR = {Rudolph Bergahmmer and Yassine Lakhnech}
}

• fmtools99.pdf
• fmtools99.ps