Top

Published in:

2019 | OriginalPaper | Chapter

Bounded Exhaustive Testing with Certified and Optimized Data Enumeration Programs

Authors : Clotilde Erard, Alain Giorgetti

Published in: Testing Software and Systems

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Performance Comparison of Two Search-Based Testing Strategies for ADAS System Validation

next chapter A Mechanised Proof of an Adaptive State Counting Algorithm

The work presented in this paper is in release 1.2 of ENUM.

http://compcert.inria.fr/compcert-C.html.

QuviQ testing tools (2019). http://www.quviq.com

Arndt, J.: Matters Computational - Ideas, Algorithms, Source Code [The fxtbook] (2010). https://www.jjj.de/fxt/fxtpage.html

Bobot, F., Filliâtre, J.-C., Marché, C., Melquiond, G., Paskevich, A.: The Why3 Platform (2018). http://why3.lri.fr/manual.pdf

Bulwahn, L.: The new Quickcheck for Isabelle - random, exhaustive and symbolic testing under one roof. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 92–108. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35308-6_10CrossRefMATH

Dailler, S., Hauzar, D., Marché, C., Moy, Y.: Instrumenting a weakest precondition calculus for counterexample generation. J. Logic Algebraic Methods Program. 99, 97–113 (2018). https://doi.org/10.1016/j.jlamp.2018.05.003MathSciNetCrossRefMATH

Dubois, C., Giorgetti, A.: Tests and proofs for custom data generators. Formal Aspects Comput. 30, 659–684 (2018)MathSciNetCrossRef

Dubois, C., Giorgetti, A., Genestier, R.: Tests and proofs for enumerative combinatorics. In: Aichernig, B.K.K., Furia, C.A.A. (eds.) TAP 2016. LNCS, vol. 9762, pp. 57–75. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41135-4_4CrossRefMATH

Filliâtre, J.-C., Pereira, M.: Itérer avec confiance. In: Journées Francophones des Langages Applicatifs (JFLA 2016) (2016). https://hal.inria.fr/hal-01240891

Filliâtre, J.-C., Pereira, M.: A modular way to reason about iteration. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 322–336. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40648-0_24CrossRef

10.

Genestier, R., Giorgetti, A., Petiot, G.: Sequential generation of structured arrays and its deductive verification. In: Blanchette, J.C., Kosmatov, N. (eds.) TAP 2015. LNCS, vol. 9154, pp. 109–128. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21215-9_7CrossRef

11.

Giorgetti, A., Lazarini, R.: Preuve de programmes d’énumération avec Why3. In: AFADL 2018, pp. 14–19 (2018). http://afadl2018.ls2n.fr/wp-content/uploads/sites/38/2018/06/AFADL_Procs_2018.pdf

12.

Giorgetti, A., Dubois, C., Lazarini, R.: Combinatoire formelle avec Why3 et Coq. In: Journées Francophones des Langages Applicatifs (JFLA 2019), Les Rousses, France, pp. 139–154, January 2019. https://hal.inria.fr/hal-01985195

13.

Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J. Formaliz. Reason. 3, 95–152 (2010)MathSciNetMATH

14.

Hriţcu, C., Lampropoulos, L., Dénès, M., Paraskevopoulou, Z.: QuickChick: randomized property-based testing plugin for Coq (2018). https://github.com/QuickChick/QuickChick

15.

Jackson, D., Damon, C.: Elements of style: analyzing a software design feature with a counterexample detector. IEEE Trans. Softw. Eng. 22(7), 484–495 (1996)CrossRef

16.

Leino, K.R.M., Moskal, M.: Usable auto-active verification. In: Usable Verification Workshop (2010). http://fm.csl.sri.com/UV10/

17.

Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRef

18.

Paraskevopoulou, Z., Hriţcu, C., Dénès, M., Lampropoulos, L., Pierce, B.C.: Foundational property-based testing. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 325–343. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22102-1_22CrossRef

19.

Rieu-Helft, R., Marché, C., Melquiond, G.: How to get an efficient yet verified arbitrary-precision integer library. In: Paskevich, A., Wies, T. (eds.) VSTTE 2017. LNCS, vol. 10712, pp. 84–101. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-72308-2_6CrossRefMATH

20.

Runciman, C., Naylor, M., Lindblad, F.: Smallcheck and lazy smallcheck: automatic exhaustive testing for small values. In: Proceedings of the 1st ACM SIGPLAN Symposium on Haskell, pp. 37–48. ACM (2008). https://doi.org/10.1145/1411286.1411292

21.

Sullivan, K.J., Yang, J., Coppit, D., Khurshid, S., Jackson, D.: Software assurance by bounded exhaustive testing. In: Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, pp. 133–142. ACM (2004)

Title: Bounded Exhaustive Testing with Certified and Optimized Data Enumeration Programs
Authors: Clotilde Erard
Alain Giorgetti
Publisher: Springer International Publishing
Book: Testing Software and Systems
Print ISBN: 978-3-030-31279-4

Electronic ISBN: 978-3-030-31280-0

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-31280-0_10

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner