Generating Unit Tests from Formal Proofs
- Author(s):
-
Source:
International Conference on Tests And Proofs (TAP), ETH Zürich, Switzerland, 2007
-
We present a new automatic test generation method for JAVA CARD based on attempts at formal verification of the implementation under test (IUT). Self-contained unit tests in JUnit format are generated automatically. The advantages of the approach are: (i) it exploits the full information available in the IUT and in its formal model giving very good hybrid coverage; (ii) a non-trivial formal model of the IUT is unnecessary; (iii) it is adaptable to the skills that users may possess in formal methods.
BibTeX
@inproceedings{engelHaehnle07,
author = {Christian Engel and Reiner H{\"a}hnle},
title = {Generating Unit Tests from Formal Proofs},
booktitle = {Proceedings, 1st International Conference on Tests And Proofs (TAP), Zurich, Switzerland},
editor = {Yuri Gurevich and Bertrand Meyer},
year = {2007},
series = {LNCS},
volume = {4454},
publisher = {Springer}
}