Logic and Formal Methods

Generating Unit Tests from Formal Proofs

  • Author(s):

    Christian Engel
    Reiner Hähnle

  • 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.


    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}