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

https://hal.inria.fr/hal-02526343
Contributor : Hal Ifip <>
Submitted on : Tuesday, March 31, 2020 - 3:13:25 PM
Last modification on : Tuesday, March 31, 2020 - 4:02:13 PM

File

 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

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

54