Document Open Access Logo

Automated Random Testing of Numerical Constrained Types

Authors Ghiles Ziat, Matthieu Dien, Vincent Botbol

PDF
Thumbnail PDF

File

LIPIcs.CP.2021.59.pdf
  • Filesize: 0.79 MB
  • 19 pages

Document Identifiers

Author Details

Ghiles Ziat
  • ISAE-SUPAERO, Université de Toulouse, France
Matthieu Dien
  • Université de Caen, France
Vincent Botbol
  • Nomadic labs, Paris, France

Funding

This work has been partially supported by the Defense Innovation Agency (AID) of the French Ministry of Defense under Grant No.: 2018.60.0072.00.470.75.01 and the RIN ALENOR project.

Cite AsGet BibTex

Ghiles Ziat, Matthieu Dien, and Vincent Botbol. Automated Random Testing of Numerical Constrained Types. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 59:1-59:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CP.2021.59

Abstract

We propose an automated testing framework based on constraint programming techniques. Our framework allows the developer to attach a numerical constraint to a type that restricts its set of possible values. We use this constraint as a partial specification of the program, our goal being to derive property-based tests on such annotated programs. To achieve this, we rely on the user-provided constraints on the types of a program: for each function f present in the program, that returns a constrained type, we generate a test. The tests consists of generating uniformly pseudo-random inputs and checking whether f’s output satisfies the constraint. We are able to automate this process by providing a set of generators for primitive types and generator combinators for composite types. To derive generators for constrained types, we present in this paper a technique that characterizes their inhabitants as the solution set of a numerical CSP. This is done by combining abstract interpretation and constraint solving techniques that allow us to efficiently and uniformly generate solutions of numerical CSP. We validated our approach by implementing it as a syntax extension for the OCaml language.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Dynamic analysis
Keywords
  • Constraint Programming
  • Automated Random Testing
  • Abstract Domains
  • Constrained Types

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Ignacio Araya, Gilles Trombettoni, and Bertrand Neveu. Exploiting Monotonicity in Interval Constraint Propagation. In Association for the Advancement of Artificial Intelligence, editor, Twenty-Fourth AAAI Conference on Artificial Intelligence, pages 9-14, Atlanta, United States, July 2010. http://www.aaai.org/ocs/index.php/AAAI/AAAI10/paper/view/1699. URL: https://hal-enpc.archives-ouvertes.fr/hal-00654400.
  2. Lennart Augustsson. Cayenne - a language with dependent types. In S. Doaitse Swierstra, José N. Oliveira, and Pedro R. Henriques, editors, Advanced Functional Programming, pages 240-267, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. Google Scholar
  3. Frédéric Benhamou, Frédéric Goualard, Laurent Granvilliers, and Jean-Francois Puget. Revising hull and box consistency. In Logic Programming: Proceedings of the 1999 International Conference on Logic Programming, pages 230-244, January 1999. Google Scholar
  4. G. Brightwell and P. Winkler. Counting linear extensions is ♯p-complete. In STOC '91, 1991. Google Scholar
  5. Jacob Burnim, Sudeep Juvekar, and Koushik Sen. Wise: Automated test generation for worst-case complexity. In Proceedings of the 31st International Conference on Software Engineering, ICSE '09, page 463–473, New York, NY, USA, 2009. Association for Computing Machinery. URL: https://doi.org/10.1109/ICSE.2009.5070545.
  6. Benjamin Canou and Alexis Darrasse. Fast and sound random generation for automated testing and benchmarking in objective caml. In Proceedings of the 2009 ACM SIGPLAN Workshop on ML, ML '09, page 61–70, New York, NY, USA, 2009. Association for Computing Machinery. URL: https://doi.org/10.1145/1596627.1596637.
  7. Matthieu Carlier, Catherine Dubois, and Arnaud Gotlieb. Focaltest: A constraint programming approach for property-based testing. In José Cordeiro, Maria Virvou, and Boris Shishkov, editors, Software and Data Technologies, pages 140-155, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  8. Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. A scalable and nearly uniform generator of sat witnesses. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification, pages 608-623, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  9. Koen Claessen and John Hughes. Quickcheck: A lightweight tool for random testing of haskell programs. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, ICFP '00, page 268–279, New York, NY, USA, 2000. Association for Computing Machinery. URL: https://doi.org/10.1145/351240.351266.
  10. Benjamin Cousins. Efficient high-dimensional sampling and integration. PhD thesis, Georgia Institute of Technology, 2017. Google Scholar
  11. Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238-252, 1977. Google Scholar
  12. Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 84-96, 1978. Google Scholar
  13. Simon Cruanes. QuickCheck inspired property-based testing for OCaml. URL: https://github.com/c-cube/qcheck.
  14. Rafael Dutra, Kevin Laeufer, Jonathan Bachrach, and Koushik Sen. Efficient sampling of sat solutions for testing. In 2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE), ICSE '18, page 549–559, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3180155.3180248.
  15. Peter Dybjer, Qiao Haiyan, and Makoto Takeyama. Random generators for dependent types. In Zhiming Liu and Keijiro Araki, editors, Theoretical Aspects of Computing - ICTAC 2004, pages 341-355, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  16. Patrice Godefroid, Nils Klarlund, and Koushik Sen. Dart: Directed automated random testing. SIGPLAN Not., 40(6):213–223, 2005. URL: https://doi.org/10.1145/1064978.1065036.
  17. Vibhav Gogate and Rina Dechter. A new algorithm for sampling csp solutions uniformly at random. In Frédéric Benhamou, editor, Principles and Practice of Constraint Programming - CP 2006, pages 711-715, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  18. A. Gotlieb, B. Botella, and M. Watel. Inka: Ten years after the first ideas. In 19th International Conference on Software & Systems Engineering and their Applications (ICSSEA'06), Paris, France, December 2006. Google Scholar
  19. Erwan Jahier and Pascal Raymond. Generating random values using Binary Decision Diagrams and Convex Polyhedra. In Frédéric Benhamou, Narendra Jussien, and Barry O'Sullivan, editors, Trends in Constraint Programming, page 416 pp. ISTE, 2007. URL: https://hal.archives-ouvertes.fr/hal-00389766.
  20. Bertrand Jeannet and Antoine Miné. Apron: A library of numerical abstract domains for static analysis. In Proceedings of the 21th International Conference Computer Aided Verification (CAV 2009), 2009. Google Scholar
  21. Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. The ocaml system release 4.02. Institut National de Recherche en Informatique et en Automatique, 54, 2014. Google Scholar
  22. Alexandre Maréchal, Alexis Fouilhé, Tim King, David Monniaux, and Michaël Périn. Polyhedral approximation of multivariate polynomials using handelman’s theorem. In 17th International Conference on Verification, Model Checking, and Abstract Interpretation, pages 166-184, 2016. Google Scholar
  23. Jan Midtgaard. Quickchecking patricia trees. In Meng Wang and Scott Owens, editors, Trends in Functional Programming, pages 59-78, Cham, 2018. Springer International Publishing. Google Scholar
  24. Jan Midtgaard, Mathias Justesen, Patrick Kasting, Flemming Nielson, and Hanne Nielson. Effect-driven quickchecking of compilers. Proceedings of the ACM on Programming Languages, 1:1-23, August 2017. URL: https://doi.org/10.1145/3110259.
  25. Antoine Miné. Symbolic methods to enhance the precision of numerical abstract domains. In 7th International Conference on Verification, Model Checking, and Abstract Interpretation, 2006. Google Scholar
  26. Ugo Montanari. Networks of constraints: Fundamental properties and applications to picture processing. Information Science, 7(2):95-132, 1974. Google Scholar
  27. Martin Odersky, Martin Sulzmann, and Martin Wehr. Type inference with constrained types. TAPOS, 5:35-55, January 1999. URL: https://doi.org/10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4.
  28. Michal Palka, Koen Claessen, Alejandro Russo, and John Hughes. Testing an optimising compiler by generating random lambda terms. Proceedings - International Conference on Software Engineering, January 2011. URL: https://doi.org/10.1145/1982595.1982615.
  29. Marie Pelleau, Antoine Miné, Charlotte Truchet, and Frédéric Benhamou. A constraint solver based on abstract domains. In Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2013), 2013. Google Scholar
  30. G. Pesant. Counting solutions of csps: A structural approach. In IJCAI, 2005. Google Scholar
  31. F. Pottier. Strong automated testing of ocaml libraries. In JFLA 2021 - 32es Journées Francophones des Langages Applicatifs, 2020. Google Scholar
  32. Xavier Rival. Understanding the origin of alarms in astrée. In Chris Hankin and Igor Siveroni, editors, Static Analysis, pages 303-319, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  33. Colin Runciman, Matthew Naylor, and Fredrik Lindblad. Smallcheck and lazy smallcheck automatic exhaustive testing for small values. In Proceedings of the First ACM SIGPLAN Symposium on Haskell, volume 44, pages 37-48, January 2008. Google Scholar
  34. Pascal Sotin. Quantifying the precision of numerical abstract domains, 2010. URL: https://hal.inria.fr/inria-00457324.
  35. Charlotte Truchet, Marie Pelleau, and Frédéric Benhamou. Abstract domains for constraint programming, with the example of octagons. International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pages 72-79, 2010. URL: https://doi.org/10.1109/SYNASC.2010.69.
  36. H. Xi. Dependent ml an approach to practical programming with dependent types. J. Funct. Program., 17:215-286, 2007. Google Scholar
  37. M Zalewski. American fuzzy lop. URL: https://lcamtuf.coredump.cx/afl/.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact