Bounded Exhaustive Testing with Certified and Optimized Data Enumeration Programs
| Affiliation auteurs | !!!! Error affiliation !!!! |
| Titre | Bounded Exhaustive Testing with Certified and Optimized Data Enumeration Programs |
| Type de publication | Conference Paper |
| Year of Publication | 2019 |
| Auteurs | Erard C, Giorgetti A |
| Editor | Gaston C, Kosmatov N, LeGall P |
| Conference Name | TESTING SOFTWARE AND SYSTEMS (ICTSS 2019) |
| Publisher | Int Federat Informat Proc Working Grp 6 1; CEA Tech, List Inst; CentraleSupelec; Telecom ParisTech; CNRS, French Network Software Engn & Programming; Univ Paris Saclay |
| Conference Location | GEWERBESTRASSE 11, CHAM, CH-6330, SWITZERLAND |
| ISBN Number | 978-3-030-31280-0; 978-3-030-31279-4 |
| Mots-clés | Algorithmic efficiency, Bounded exhaustive testing, formal verification |
| Résumé | Bounded exhaustive testing (BET) is an elementary technique in automated unit testing. It consists in testing a function with all input data up to a given size bound. We implement BET to check logical and program properties, before attempting to prove them formally with the deductive verification tool Why3. We also present a library of enumeration programs for BET, certified by formal proofs of their properties with Why3. In order to make BET more efficient, we study and compare several strategies to optimize these programs. |
| DOI | 10.1007/978-3-030-31280-0_10 |