%0 Conference Proceedings
%T Bounded Exhaustive Testing with Certified and Optimized Data Enumeration Programs
%+ Université Bourgogne Franche-Comté [COMUE] (UBFC)
%A Erard, Clotilde
%A Giorgetti, Alain
%Z Part 4: Testing and Verification Techniques
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 31th IFIP International Conference on Testing Software and Systems (ICTSS)
%C Paris, France
%Y Christophe Gaston
%Y Nikolai Kosmatov
%Y Pascale Le Gall
%I Springer International Publishing
%3 Testing Software and Systems
%V LNCS-11812
%P 159-175
%8 2019-10-15
%D 2019
%R 10.1007/978-3-030-31280-0_10
%K Bounded exhaustive testing
%K Formal verification
%K Algorithmic efficiency
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-02526343/document
%2 https://inria.hal.science/hal-02526343/file/482770_1_En_10_Chapter.pdf
%L hal-02526343
%U https://inria.hal.science/hal-02526343
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-ICTSS
%~ IFIP-LNCS-11812