Skip to Main content Skip to Navigation
Conference papers

Bounded Exhaustive Testing with Certified and Optimized Data Enumeration Programs

Abstract : 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.
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Tuesday, March 31, 2020 - 3:13:25 PM
Last modification on : Tuesday, March 31, 2020 - 4:02:13 PM


 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2022-01-01

Please log in to resquest access to the document


Distributed under a Creative Commons Attribution 4.0 International License



Clotilde Erard, Alain Giorgetti. Bounded Exhaustive Testing with Certified and Optimized Data Enumeration Programs. 31th IFIP International Conference on Testing Software and Systems (ICTSS), Oct 2019, Paris, France. pp.159-175, ⟨10.1007/978-3-030-31280-0_10⟩. ⟨hal-02526343⟩



Record views