Document Open Access Logo

Mutational Fuzz Testing for Constraint Modeling Systems

Authors Wout Vanroose , Ignace Bleukx , Jo Devriendt , Dimos Tsouros , Hélène Verhaeghe , Tias Guns

PDF
Thumbnail PDF

File

LIPIcs.CP.2024.29.pdf
  • Filesize: 0.85 MB
  • 25 pages

Document Identifiers

Author Details

Wout Vanroose
  • DTAI, KU Leuven, Belgium
Ignace Bleukx
  • DTAI, KU Leuven, Belgium
Jo Devriendt
  • DTAI, KU Leuven, Belgium
Dimos Tsouros
  • DTAI, KU Leuven, Belgium
Hélène Verhaeghe
  • DTAI, KU Leuven, Belgium
Tias Guns
  • DTAI, KU Leuven, Belgium

Funding

This research received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (Grant No. 101002802, CHAT-Opt).

Cite AsGet BibTex

Wout Vanroose, Ignace Bleukx, Jo Devriendt, Dimos Tsouros, Hélène Verhaeghe, and Tias Guns. Mutational Fuzz Testing for Constraint Modeling Systems. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 29:1-29:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CP.2024.29

Abstract

Constraint programming (CP) modeling languages, like MiniZinc, Essence and CPMpy, play a crucial role in making CP technology accessible to non-experts. Both solver-independent modeling frameworks and solvers themselves are complex pieces of software that can contain bugs, which undermines their usefulness. Mutational fuzz testing is a way to test complex systems by stochastically mutating input and verifying preserved properties of the mutated output. We investigate different mutations and verification methods that can be used on the constraint specifications directly. This includes methods proposed in the context of SMT problem specifications, as well as new methods related to global constraints, optimization, and solution counting/preservation. Our results show that such a fuzz testing approach improves the overall code coverage of a modeling system compared to only unit testing, and is able to find bugs in the whole toolchain, from the modeling language transformations themselves to the underlying solvers.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • fuzz testing
  • Constraint modeling language
  • bugs
  • mutational testing
  • modeling
  • constraint reformulation

Metrics

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

Supplementary Materials

References

  1. Abderrahmane Aggoun and Nicolas Beldiceanu. Extending CHIP in order to solve complex scheduling and placement problems. In Jean-Paul Delahaye, Philippe Devienne, Philippe Mathieu, and Pascal Yim, editors, JFPL'92, 1ères Journées Francophones de Programmation Logique, 25-27 Mai 1992, Lille, France, page 51, 1992. Google Scholar
  2. Özgür Akgün, Alan M. Frisch, Ian P. Gent, Christopher Jefferson, Ian Miguel, and Peter Nightingale. Conjure: Automatic generation of constraint models from problem specifications. Artif. Intell., 310:103751, 2022. URL: https://doi.org/10.1016/j.artint.2022.103751.
  3. Özgür Akgün, Ian P. Gent, Christopher Jefferson, Ian Miguel, and Peter Nightingale. Metamorphic testing of constraint solvers. In John N. Hooker, editor, Principles and Practice of Constraint Programming - 24th International Conference, CP 2018, Lille, France, August 27-31, 2018, Proceedings, volume 11008 of Lecture Notes in Computer Science, pages 727-736. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98334-9_46.
  4. Mario Alviano, Carmine Dodaro, Johannes Klaus Fichte, Markus Hecher, Tobias Philipp, and Jakob Rath. Inconsistency proofs for ASP: the ASP - DRUPE format. Theory Pract. Log. Program., 19(5-6):891-907, 2019. URL: https://doi.org/10.1017/S1471068419000255.
  5. Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, and Clark W. Barrett. Flexible proof production in an industrial-strength SMT solver. In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 15-35. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_3.
  6. Nicolas Beldiceanu, Mats Carlsson, and Jean-Xavier Rampon. Global constraint catalog, (revision a), 2012. Google Scholar
  7. Gleb Belov, Peter J. Stuckey, Guido Tack, and Mark Wallace. Improved linearization of constraint programming models. In Michel Rueher, editor, Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings, volume 9892 of Lecture Notes in Computer Science, pages 49-65. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-44953-1_4.
  8. Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified symmetry and dominance breaking for combinatorial optimisation. In Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 - March 1, 2022, pages 3698-3707. AAAI Press, 2022. URL: https://ojs.aaai.org/index.php/AAAI/article/view/20283, URL: https://doi.org/10.1609/AAAI.V36I4.20283.
  9. Mauro Bringolf. Fuzz-testing smt solvers with formula weakening and strengthening. Master’s thesis, ETH Zurich, 2021. Google Scholar
  10. Robert Brummayer and Armin Biere. Fuzzing and delta-debugging smt solvers. In Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, pages 1-5, 2009. Google Scholar
  11. Robert Brummayer, Florian Lonsing, and Armin Biere. Automated testing and debugging of SAT and QBF solvers. In Ofer Strichman and Stefan Szeider, editors, Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6175 of Lecture Notes in Computer Science, pages 44-57. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14186-7_6.
  12. Nadia Creignou and Miki Hermann. Complexity of generalized satisfiability counting problems. Inf. Comput., 125(1):1-12, 1996. URL: https://doi.org/10.1006/inco.1996.0016.
  13. Ermira Daka and Gordon Fraser. A survey on unit testing practices and problems. In 25th IEEE International Symposium on Software Reliability Engineering, ISSRE 2014, Naples, Italy, November 3-6, 2014, pages 201-211. IEEE Computer Society, 2014. URL: https://doi.org/10.1109/ISSRE.2014.11.
  14. Xavier Gillard, Pierre Schaus, and Yves Deville. Solvercheck: Declarative testing of constraints. In Thomas Schiex and Simon de Givry, editors, Principles and Practice of Constraint Programming, pages 565-582, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-30048-7_33.
  15. Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Veripb: The easy way to make your combinatorial search algorithm trustworthy. In workshop From Constraint Programming to Trustworthy AI at the 26th International Conference on Principles and Practice of Constraint Programming (CP’20). Paper available at http://www. cs. ucc. ie/bg6/cptai/2020/papers/CPTAI_2020_paper_2. pdf, 2020. Google Scholar
  16. Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. An auditable constraint programming solver. In Christine Solnon, editor, 28th International Conference on Principles and Practice of Constraint Programming, CP 2022, July 31 to August 8, 2022, Haifa, Israel, volume 235 of LIPIcs, pages 25:1-25:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CP.2022.25.
  17. Tias Guns. Increasing modeling language convenience with a universal n-dimensional array, cppy as python-embedded example. In Proceedings of the 18th workshop on Constraint Modelling and Reformulation at CP (Modref 2019), volume 19, 2019. Google Scholar
  18. Marijn J. H. Heule. Proofs of unsatisfiability. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 635-668. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200998.
  19. Ahmet B. Keha, Ketan Khowala, and John W. Fowler. Mixed integer programming formulations for single machine scheduling problems. Comput. Ind. Eng., 56(1):357-367, 2009. URL: https://doi.org/10.1016/j.cie.2008.06.008.
  20. Ruben Kindt and Mattias Guns. Fuzz testing of constraint programming. Master’s thesis, KU Leuven, 2023. URL: https://kuleuven.limo.libis.be/discovery/fulldisplay?docid=alma9993364582101488&context=L&vid=32KUL_KUL:KULeuven&search_scope=All_Content&tab=all_content_tab&lang=en.
  21. Shuvendu K. Lahiri and Shaz Qadeer. Back to the future: revisiting precise program verification using SMT solvers. In George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 171-182. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328461.
  22. Stephan Lukasczyk, Florian Kroiß, and Gordon Fraser. Automated unit test generation for python. CoRR, abs/2007.14049, 2020. URL: https://arxiv.org/abs/2007.14049.
  23. Muhammad Numair Mansur, Maria Christakis, Valentin Wüstholz, and Fuyuan Zhang. Detecting critical bugs in SMT solvers using blackbox mutational fuzzing. In Prem Devanbu, Myra B. Cohen, and Thomas Zimmermann, editors, ESEC/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Virtual Event, USA, November 8-13, 2020, pages 701-712. ACM, 2020. URL: https://doi.org/10.1145/3368089.3409763.
  24. Matthew J. McIlree and Ciaran McCreesh. Proof logging for smart extensional constraints. In Roland H. C. Yap, editor, 29th International Conference on Principles and Practice of Constraint Programming, CP 2023, August 27-31, 2023, Toronto, Canada, volume 280 of LIPIcs, pages 26:1-26:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CP.2023.26.
  25. Barton P. Miller, Lars Fredriksen, and Bryan So. An empirical study of the reliability of UNIX utilities. Commun. ACM, 33(12):32-44, 1990. URL: https://doi.org/10.1145/96267.96279.
  26. Nicholas Nethercote, Peter J. Stuckey, Ralph Becket, Sebastian Brand, Gregory J. Duck, and Guido Tack. Minizinc: Towards a standard CP modelling language. In Christian Bessiere, editor, Principles and Practice of Constraint Programming - CP 2007, 13th International Conference, CP 2007, Providence, RI, USA, September 23-27, 2007, Proceedings, volume 4741 of Lecture Notes in Computer Science, pages 529-543. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74970-7_38.
  27. Peter Nightingale, Özgür Akgün, Ian P. Gent, Christopher Jefferson, and Ian Miguel. Automatically improving constraint models in savile row through associative-commutative common subexpression elimination. In Barry O'Sullivan, editor, Principles and Practice of Constraint Programming - 20th International Conference, CP 2014, Lyon, France, September 8-12, 2014. Proceedings, volume 8656 of Lecture Notes in Computer Science, pages 590-605. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-10428-7_43.
  28. Peter Nightingale, Patrick Spracklen, and Ian Miguel. Automatically improving SAT encoding of constraint problems through common subexpression elimination in savile row. In Gilles Pesant, editor, Principles and Practice of Constraint Programming - 21st International Conference, CP 2015, Cork, Ireland, August 31 - September 4, 2015, Proceedings, volume 9255 of Lecture Notes in Computer Science, pages 330-340. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23219-5_23.
  29. Tobias Paxian and Armin Biere. Uncovering and classifying bugs in maxsat solvers through fuzzing and delta debugging. Update reference when published, 2022. URL: http://www.pragmaticsofsat.org/2023/live/POS23_paper_4.pdf.
  30. Andrea Rendl. Effective compilation of constraint models. PhD thesis, University of St Andrews, UK, 2010. URL: https://hdl.handle.net/10023/973.
  31. Robert Robere, Antonina Kolokolova, and Vijay Ganesh. The proof complexity of SMT solvers. In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, volume 10982 of Lecture Notes in Computer Science, pages 275-293. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96142-2_18.
  32. Francesca Rossi, Peter van Beek, and Toby Walsh, editors. Handbook of Constraint Programming, volume 2 of Foundations of Artificial Intelligence. Elsevier, 2006. URL: https://www.sciencedirect.com/science/bookseries/15746526/2.
  33. Olivier Roussel and Christophe Lecoutre. XML representation of constraint networks: Format XCSP 2.1. CoRR, abs/0902.2362, 2009. URL: https://arxiv.org/abs/0902.2362.
  34. Gilles Simonin, Christian Artigues, Emmanuel Hebrard, and Pierre Lopez. Scheduling scientific experiments for comet exploration. Constraints An Int. J., 20(1):77-99, 2015. URL: https://doi.org/10.1007/S10601-014-9169-3.
  35. Hussain Bilal Syed. Model selection and testing for an automated constraint modelling toolchain. PhD thesis, University of St Andrews, UK, 2017. URL: https://hdl.handle.net/10023/10328.
  36. Petar Tahchiev, Felipe Leme, Vincent Massol, and Gary Gregory. JUnit in Action, 2nd Edition. Manning Publications Company, 2011. URL: https://www.manning.com/books/junit-in-action-second-edition.
  37. Willem Jan van Hoeve. The alldifferent constraint: A survey. CoRR, cs.PL/0105015, 2001. URL: https://arxiv.org/abs/cs/0105015.
  38. Willem-Jan van Hoeve and Irit Katriel. Global constraints. In Francesca Rossi, Peter van Beek, and Toby Walsh, editors, Handbook of Constraint Programming, volume 2 of Foundations of Artificial Intelligence, pages 169-208. Elsevier, 2006. URL: https://doi.org/10.1016/S1574-6526(06)80010-6.
  39. Dieter Vandesande, Wolf De Wulf, and Bart Bogaerts. Qmaxsatpb: A certified maxsat solver. In Georg Gottlob, Daniela Inclezan, and Marco Maratea, editors, Logic Programming and Nonmonotonic Reasoning - 16th International Conference, LPNMR 2022, Genova, Italy, September 5-9, 2022, Proceedings, volume 13416 of Lecture Notes in Computer Science, pages 429-442. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-15707-3_33.
  40. T.W. Williams, M.R. Mercer, J.P. Mucha, and R. Kapur. Code coverage, what does it mean in terms of quality? In Annual Reliability and Maintainability Symposium. 2001 Proceedings. International Symposium on Product Quality and Integrity (Cat. No.01CH37179), pages 420-424, 2001. URL: https://doi.org/10.1109/RAMS.2001.902502.
  41. Dominik Winterer, Chengyu Zhang, and Zhendong Su. On the unusual effectiveness of type-aware operator mutations for testing SMT solvers. Proc. ACM Program. Lang., 4(OOPSLA):193:1-193:25, 2020. URL: https://doi.org/10.1145/3428261.
  42. Dominik Winterer, Chengyu Zhang, and Zhendong Su. Validating SMT solvers via semantic fusion. In Alastair F. Donaldson and Emina Torlak, editors, Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, pages 718-730. ACM, 2020. URL: https://doi.org/10.1145/3385412.3385985.
  43. Hui Ye, Shaoyin Cheng, Lanbo Zhang, and Fan Jiang. Droidfuzzer: Fuzzing the android apps with intent-filter tag. In René Mayrhofer, Luke Chen, Matthias Steinbauer, Gabriele Kotsis, and Ismail Khalil, editors, The 11th International Conference on Advances in Mobile Computing & Multimedia, MoMM '13, Vienna, Austria, December 2-4, 2013, page 68. ACM, 2013. URL: https://doi.org/10.1145/2536853.2536881.
  44. Andreas Zeller. Yesterday, my program worked. today, it does not. why? In Oscar Nierstrasz and Michel Lemoine, editors, Software Engineering - ESEC/FSE'99, 7th European Software Engineering Conference, Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Toulouse, France, September 1999, Proceedings, volume 1687 of Lecture Notes in Computer Science, pages 253-267. Springer, 1999. URL: https://doi.org/10.1007/3-540-48166-4_16.
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