[en] We present a technique that enables us to distinguish valid from invalid data structure objects. The technique is based on building an artificial neural network, more precisely a binary classifier, and training it to identify valid and invalid instances of a data structure. The obtained classifier can then be used in place of the data structure’s invariant, in order to attempt to identify (in)correct behaviors in programs manipulating the structure. In order to produce the valid objects to train the network, an assumed-correct set of object building routines is randomly executed. Invalid instances are produced by generating values for object fields that “break” the collected valid values, i.e., that assign values to object fields that have not been observed as feasible in the assumed-correct program executions that led to the collected valid instances. We experimentally assess this approach, over a benchmark of data structures. We show that this learning technique produces classifiers that achieve significantly better accuracy in classifying valid/invalid objects compared to a technique for dynamic invariant detection, and leads to improved bug finding.
Disciplines :
Computer science
Author, co-author :
Molina, Facundo
Degiovanni, Renzo Gaston ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
Ponzio, Pablo
Regis, Germán
Aguirre, Nazareno
Frias, Marcelo F.
External co-authors :
yes
Language :
English
Title :
Training binary classifiers as data structure invariants
Publication date :
2019
Event name :
41st International Conference on Software Engineering ICSE 2019
Event date :
May 25-31, 2019
Audience :
International
Main work title :
Proceedings of the 41st International Conference on Software Engineering ICSE 2019, Montreal, QC, Canada, May 25-31, 2019
Fibonacci heap implementation from the graphmaker library. https://github. com/nlfiedler/graphmaker. Version control revision of the bug: https://github. com/nlfiedler/graphmaker/ commit/13d53e3c314d58cb48a6186437a36241842c98d7# diff-1c644baf14f6ab27ffa2691c9ff02cbd. Accessed: 2018-09-02.
Home page of the korat test generation tool. http://korat. sourceforge. net. Accessed: 2017-07-01.
Replication package of the object (in)validity learning approach. https: //sites. google. com/site/learninginvariants.
Pablo Abad, Nazareno Aguirre, Valeria S. Bengolea, Daniel Ciolek, Marcelo F. Frias, Juan P. Galeotti, Tom Maibaum, Mariano M. Moscato, Nicolás Rosner, and Ignacio Vissani. Improving test generation under rich contracts by tight bounds and incremental SAT solving. In Sixth IEEE International Conference on Software Testing, Verification and Validation, ICST 2013, Luxembourg, Luxembourg, March 18-22, 2013, pages 21-30. IEEE Computer Society, 2013.
Mike Barnett. Code contracts for. net: Runtime verification and so much more. In Howard Barringer, Yliès Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, Gordon J. Pace, Grigore Rosu, Oleg Sokolsky, and Nikolai Tillmann, editors, Runtime Verification-First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings, volume 6418 of Lecture Notes in Computer Science, pages 16-17. Springer, 2010.
Earl T. Barr, Mark Harman, Phil McMinn, Muzammil Shahbaz, and Shin Yoo. The oracle problem in software testing: A survey. IEEE Trans. Software Eng., 41(5):507-525, 2015.
James Bergstra and Yoshua Bengio. Random search for hyper-parameter optimization. J. Mach. Learn. Res., 13:281-305, February 2012.
Chandrasekhar Boyapati, Sarfraz Khurshid, and Darko Marinov. Korat: automated testing based on Java predicates. In Phyllis G. Frankl, editor, Proceedings of the International Symposium on Software Testing and Analysis, ISSTA 2002, Roma, Italy, July 22-24, 2002, pages 123-133. ACM, 2002.
Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll. Beyond assertions: Advanced specification and verification with JML and esc/Java2. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever, editors, Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures, volume 4111 of Lecture Notes in Computer Science, pages 342-363. Springer, 2005.
Christoph Csallner, Nikolai Tillmann, and Yannis Smaragdakis. Dysy: dynamic symbolic execution for invariant inference. In Wilhelm Schäfer, Matthew B. Dwyer, and Volker Gruhn, editors, 30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 10-18, 2008, pages 281-290. ACM, 2008.
Greg Dennis, Felix Sheng-Ho Chang, and Daniel Jackson. Modular verification of code with SAT. In Lori L. Pollock and Mauro Pezzè, editors, Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, Portland, Maine, USA, July 17-20, 2006, pages 109-120. ACM, 2006.
Hyunsook Do, Sebastian G. Elbaum, and Gregg Rothermel. Supporting controlled experimentation with testing techniques: An infrastructure and its potential impact. Empirical Software Engineering, 10(4):405-435, 2005.
Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz, and Chen Xiao. The daikon system for dynamic detection of likely invariants. Sci. Comput. Program., 69(1-3):35-45, 2007.
Juan P. Galeotti, Nicolás Rosner, Carlos López Pombo, and Marcelo F. Frias. Analysis of invariants for efficient bounded verification. In Paolo Tonella and Alessandro Orso, editors, Proceedings of the Nineteenth International Symposium on Software Testing and Analysis, ISSTA 2010, Trento, Italy, July 12-16, 2010, pages 25-36. ACM, 2010.
Milos Gligoric, Tihomir Gvero, Vilas Jagannath, Sarfraz Khurshid, Viktor Kuncak, and Darko Marinov. Test generation through programming in UDITA. In Jeff Kramer, Judith Bishop, Premkumar T. Devanbu, and Sebastián Uchitel, editors, Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering-Volume 1, ICSE 2010, Cape Town, South Africa, 1-8 May 2010, pages 225-234. ACM, 2010.
Isabelle Guyon and André Elisseeff. An introduction to variable and feature selection. Journal of Machine Learning Research, 3:1157-1182, 2003.
Daniel Jackson. Software Abstractions-Logic, Language, and Analysis. MIT Press, 2006.
Daniel Jackson, Somesh Jha, and Craig Damon. Isomorph-free model enumeration: A new method for checking relational specifications. ACM Trans. Program. Lang. Syst., 20(2):302-343, 1998.
Shadi Abdul Khalek, Guowei Yang, Lingming Zhang, Darko Marinov, and Sarfraz Khurshid. Testera: A tool for testing Java programs using alloy specifications. In Perry Alexander, Corina S. Pasareanu, and John G. Hosking, editors, 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), Lawrence, KS, USA, November 6-10, 2011, pages 608-611. IEEE Computer Society, 2011.
Sarfraz Khurshid, Corina S. Pasareanu, and Willem Visser. Generalized symbolic execution for model checking and testing. In Hubert Garavel and John Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2619 of Lecture Notes in Computer Science, pages 553-568. Springer, 2003.
Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest, and Westley Weimer. Genprog: A generic method for automatic software repair. IEEE Trans. Software Eng., 38(1):54-72, 2012.
Barbara Liskov and John V. Guttag. Program Development in Java-Abstraction, Specification, and Object-Oriented Design. Addison-Wesley, 2001.
Kurt Mehlhorn and Peter Sanders. Algorithms and Data Structures: The Basic Toolbox. Springer, 2008.
Florian Merz, Stephan Falke, and Carsten Sinz. LLBMC: bounded model checking of C and C++ programs using a compiler IR. In Rajeev Joshi, Peter Müller, and Andreas Podelski, editors, Verified Software: Theories, Tools, Experiments-4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings, volume 7152 of Lecture Notes in Computer Science, pages 146-161. Springer, 2012.
Bertrand Meyer. Design by contract: The eiffel method. In TOOLS 1998: 26th International Conference on Technology of Object-Oriented Languages and Systems, 3-7 August 1998, Santa Barbara, CA, USA, page 446. IEEE Computer Society, 1998.
Bertrand Meyer, Ilinca Ciupa, Andreas Leitner, and Lisa Ling Liu. Automatic testing of object-oriented software. In Jan van Leeuwen, Giuseppe F. Italiano, Wiebe van der Hoek, Christoph Meinel, Harald Sack, and Frantisek Plasil, editors, SOFSEM 2007: Theory and Practice of Computer Science, 33rd Conference on Current Trends in Theory and Practice of Computer Science, Harrachov, Czech Republic, January 20-26, 2007, Proceedings, volume 4362 of Lecture Notes in Computer Science, pages 114-129. Springer, 2007.
Aditya V. Nori, Sriram K. Rajamani, SaiDeep Tetali, and Aditya V. Thakur. The yogiproject: Software property checking via static analysis and testing. In Stefan Kowalewski and Anna Philippou, editors, Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5505 of Lecture Notes in Computer Science, pages 178-181. Springer, 2009.
Carlos Pacheco, Shuvendu K. Lahiri, Michael D. Ernst, and Thomas Ball. Feedback-directed random test generation. In 29th International Conference on Software Engineering (ICSE 2007), Minneapolis, MN, USA, May 20-26, 2007, pages 75-84. IEEE Computer Society, 2007.
Corina S. Pasareanu, Willem Visser, David H. Bushnell, Jaco Geldenhuys, Peter C. Mehlitz, and Neha Rungta. Symbolic pathfinder: integrating symbolic execution with model checking for Java bytecode analysis. Autom. Softw. Eng., 20(3):391-425, 2013.
F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, P. Prettenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay. Scikit-learn: Machine learning in Python. Journal of Machine Learning Research, 12:2825-2830, 2011.
Yu Pei, Carlo A. Furia, Martin Nordio, Yi Wei, Bertrand Meyer, and Andreas Zeller. Automated fixing of programs with contracts. IEEE Trans. Software Eng., 40(5):427-449, 2014.
Pablo Ponzio, Nazareno Aguirre, Marcelo F. Frias, and Willem Visser. Field-exhaustive testing. In Thomas Zimmermann, Jane Cleland-Huang, and Zhendong Su, editors, Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, November 13-18, 2016, pages 908-919. ACM, 2016.
Stuart J. Russell and Peter Norvig. Artificial Intelligence-A Modern Approach (3. internat. ed.). Pearson Education, 2010.
Seyed Reza Shahamiri, Wan M. N. Wan-Kadir, Suhaimi Ibrahim, and Siti Zaiton Mohd Hashim. Artificial neural networks as multi-networks automated test oracle. Autom. Softw. Eng., 19(3):303-334, 2012.
Seyed Reza Shahamiri, Wan Mohd Nasir Wan-Kadir, Suhaimi Ibrahim, and Siti Zaiton Mohd Hashim. An automated framework for software test oracle. Information & Software Technology, 53(7):774-788, 2011.
Rahul Sharma and Alex Aiken. From invariant checking to invariant inference using randomized search. Formal Methods in System Design, 48(3):235-256, 2016.
Anthony J. H. Simons. Jwalk: a tool for lazy, systematic testing of Java classes by design introspection and user interaction. Autom. Softw. Eng., 14(4):369-418, 2007.
Emina Torlak and Daniel Jackson. Kodkod: A relational model finder. In Orna Grumberg and Michael Huth, editors, Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24-April 1, 2007, Proceedings, volume 4424 of Lecture Notes in Computer Science, pages 632-647. Springer, 2007.
Westley Weimer, ThanhVu Nguyen, Claire Le Goues, and Stephanie Forrest. Automatically finding patches using genetic programming. In 31st International Conference on Software Engineering, ICSE 2009, May 16-24, 2009, Vancouver, Canada, Proceedings, pages 364-374. IEEE, 2009.
W. Eric Wong, Ruizhi Gao, Yihao Li, Rui Abreu, and Franz Wotawa. A survey on software fault localization. IEEE Trans. Software En, g. 42(8):707-740, 2016.
Razieh Nokhbeh Zaeem, Divya Gopinath, Sarfraz Khurshid, and Kathryn S. McKinley. History-aware data structure repair using SAT. In Cormac Flanagan and Barbara König, editors, Tools and Algorithms for the Construction and Analysis of Systems-18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24-April 1, 2012. Proceedings, volume 7214 of Lecture Notes in Computer Science, pages 2-17. Springer, 2012.
Xiangyu Zhang, Neelam Gupta, and Rajiv Gupta. Locating faults through automated predicate switching. In Leon J. Osterweil, H. Dieter Rombach, and Mary Lou Soffa, editors, 28th International Conference on Software Engineering (ICSE 2006), Shanghai, China, May 20-28, 2006, pages 272-281. ACM, 2006.