On Theorem-proving based Testing

Abstract : HOL-TestGen is a specification and test case generation environment extending the interac- tive theorem prover Isabelle/HOL. As such, HOL-TestGen allows for an integrated workflow supporting interactive theorem proving, test case generation, and test data generation. The HOL-TestGen method is two-staged: first, the original formula is partitioned into test cases by transformation into a normal form called test theorem. Second, the test cases are analyzed for ground instances (the test data) satisfying the constraints of the test cases. Particular emphasis is put on the control of explicit test-hypotheses which can be proven over concrete programs. Due to the generality of the underlying framework, our system can be used for black-box unit, sequence, reactive sequence and white-box test scenarios. Although based on particularly clean theoretical foundations, the system can be applied for substantial case-studies.
Type de document :
Article dans une revue
Formal Aspects of Computing, Springer Verlag, 2013, 25 (5), pp.683-721. 〈http://link.springer.com/article/10.1007%2Fs00165-012-0222-y〉. 〈10.1007/s00165-012-0222-y〉
Liste complète des métadonnées

Contributeur : Burkhart Wolff <>
Soumis le : jeudi 8 octobre 2015 - 19:50:28
Dernière modification le : jeudi 11 janvier 2018 - 06:27:34




Achim D. Brucker, Burkhart Wolff. On Theorem-proving based Testing . Formal Aspects of Computing, Springer Verlag, 2013, 25 (5), pp.683-721. 〈http://link.springer.com/article/10.1007%2Fs00165-012-0222-y〉. 〈10.1007/s00165-012-0222-y〉. 〈hal-01213719〉



Consultations de la notice