Test Data Generation for Programs with Quantified First-Order Logic Specifications

Abstract : We present a novel algorithm for test data generation that is based on techniques used in formal software verification. Prominent examples of such formal techniques are symbolic execution, theorem proving, satisfiability solving, and usage of specifications and program annotations such as loop invariants. These techniques are suitable for testing of small programs, such as, e.g., implementations of algorithms, that have to be tested extremely well. In such scenarios test data is generated from test data constraints which are first-order logic formulas. These constraints are constructed from path conditions, specifications, and program annotation describing program paths that are hard to be tested randomly. A challenge is, however, to solve quantified formulas. The presented algorithm is capable of solving quantified formulas that state-of-the-art satisfiability modulo theory (SMT) solvers cannot solve. The algorithm is integrated in the formal verification and test generation tool KeY .
Type de document :
Communication dans un congrès
Alexandre Petrenko; Adenilso Simão; José Carlos Maldonado. 22nd IFIP WG 6.1 International Conference on Testing Software and Systems (ICTSS), Nov 2010, Natal, Brazil. Springer, Lecture Notes in Computer Science, LNCS-6435, pp.158-173, 2010, Testing Software and Systems. 〈10.1007/978-3-642-16573-3_12〉
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01055252
Contributeur : Hal Ifip <>
Soumis le : mardi 12 août 2014 - 09:11:35
Dernière modification le : vendredi 17 novembre 2017 - 11:56:01
Document(s) archivé(s) le : mercredi 26 novembre 2014 - 22:42:06

Fichier

paper_TML2L.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Christoph D. Gladisch. Test Data Generation for Programs with Quantified First-Order Logic Specifications. Alexandre Petrenko; Adenilso Simão; José Carlos Maldonado. 22nd IFIP WG 6.1 International Conference on Testing Software and Systems (ICTSS), Nov 2010, Natal, Brazil. Springer, Lecture Notes in Computer Science, LNCS-6435, pp.158-173, 2010, Testing Software and Systems. 〈10.1007/978-3-642-16573-3_12〉. 〈hal-01055252〉

Partager

Métriques

Consultations de la notice

103

Téléchargements de fichiers

52