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.

@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}
}