Abstract The problem of synthesizing adequate inductive invariants lies at the heart of automated software verification. The state-of-the-art machine learning algorithms for synthesizing invariants have gradually shown its excellent performance. However, synthesizing disjunctive invariants is a difficult task. In this paper, we propose a method k++ Support Vector Machine (SVM) integrating k-means++ and SVM to synthesize conjunctive and disjunctive invariants. At first, given a program, we start with executing the program to collect program states. Next, k++SVM adopts k-means++ to cluster the positive samples and then applies SVM to distinguish each positive sample cluster from all negative samples to synthesize the candidate invariants. Finally, a set of theories founded on Hoare logic are adopted to check whether the candidate invariants are true invariants. If the candidate invariants fail the check, we should sample more states and repeat our algorithm. The experimental results show that k++SVM is compatible with the algorithms for Intersection Of Half-space (IOH) and more efficient than the tool of Interproc. Furthermore, it is shown that our method can synthesize conjunctive and disjunctive invariants automatically.

References

[1] Arthur D. and Vassilvitskii S., “K-Means++: The Advantages of Careful Seeding,” in Proceedings of the 18th Annual ACM-SIAM Symposium on Discrete Algorithms, New Orleans, pp. 1027-1035, 2007.

[2] Cortes C. and Vapnik V., “Support-Vector Networks,” Machine Learning, vol. 20, no. 3, pp. 273-297, 1995.

[3] Cousot P. and Cousot R., “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints,” in Proceedings of the ACM Sigact-Sigplan Symposium on Principles of Programming Languages, New York, pp. 238-252, 1977.

[4] D'Silva V., Kroening D., and Weissenbacher G., “A Survey of Automated Techniques for Formal Software Verification,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 27, no. 7, pp. 1165-1178, 2008.

[5] Ding Z., Wang R., Hu J., and Liu Y., “Detecting Bugs of Concurrent Programs with Program Invariants,” in Proceedings of the IEEE International Conference on Software Quality, Reliability and Security Companion, Vienna, pp. 1-15, 2016.

[6] Garg P., Löding C., Madhusudan P., and Neider D., “ICE: A Robust Framework for Learning Invariants,” in Proceedings of the International Conference on Computer Aided Verification, Vienna, pp. 69-87, 2014.

[7] Garg P., “Learning-Based Inductive Invariant Synthesis,” Thesis, Univerisity of Illinois Urbana-Champaign, 2015.

[8] Garg P., Neider D., Madhusudan P., and Roth D., “Learning Invariants Using Decision Trees and Implication Counterexamples,” Acm Sigplan Notices, vol. 51, no. 1, pp. 499-512, 2015.

[9] Gulavani B., Chakraborty S., Nori A., and Rajamani S., “Automatically Refining Abstract Interpreta-tions,” in Proceedings of the Theory and Practice of Software, International Conference on TOOLS and Algorithms for the Construction and Analysis of Systems, Budapest, pp. 443-458, 2008.

[10] Gulavani B., Henzinger T., Kannan Y., and Nori A., “SYNERGY: A New Algorithm for Property Checking,” in Proceedings of the ACM Sigsoft Inter-national Symposium on Foundations of Software Engineering, Portland, pp. 117-127, 2006. Synthesizing Conjunctive and Disjunctive Linear Invariants by K-means++ and SVM 855

[11] Gulwani S., Srivastava S., and Venkatesan R., “Program Analysis as Constraint Solving,” in Proceedings of the ACM Sigplan Conference on Programming Language Design and Implementation, Tucson, pp. 281-292, 2008.

[12] Gupta A. and Rybalchenko A., “InvGen: An Efficient Invariant Generator,” in Proceedings of the International Conference on Computer Aided Verification, Grenoble, pp. 634-640, 2009.

[13] Hoare C., “An Axiomatic Basis for Computer Programming,” Communications of the ACM, vol. 12, no. 1, pp. 53-56, 1969.

[14] Jeannet B., “Interproc Analyzer for Recursive Programs with Numerical Variables,” http://popart.inrialpes.fr/interproc/interprocweb.cg i, pp. 6-11, Last Visited, 2010.

[15] Krishna S., Puhrsch C., and Wies T., “Learning Invariants using Decision Trees,” Computer Science, vol. 21, no. 7, pp. 44-59, 2015.

[16] Lin S., Sun J., Xiao H., Liu Y., Sanán D., and Hansen H., “FiB: Squeezing Loop Invariants by Interpolation between Forward/Backward Bredicate Transformers,” in Proceedings of the IEEE/ACM International Conference on Auto- mated Software Engineering, Urbana, pp. 793- 803, 2017.

[17] Li J., Sun J., Li L., and Le Q., “Automatic Loop- Invariant Generation and Refinement through Selective Sampling,” in Proceedings of the Ieee/Acm International Conference on Auto- mated Software Engineering, Buenos Aires, pp. 782-792, 2017.

[18] Jun S., Pham L., Thi L., Wang J., and Peng X., “Learning Likely Invariants to Explain Why a Program Fails,” in Proceedings of the International Conference on Engineering of Complex Computer Systems, Melbourne, pp. 70- 79, 2018.

[19] Mcdonald J., Trigg T., Roberts C., and Darden B., “Security in Agile Development: Pedagogic Lessons from an Undergraduate Software Engineering Case Study,” in Proceedings of Cyber Security Symposium, Coeur d'Alene, pp. 127-141, 2015.

[20] Mcmillan K., “Interpolation and SAT-Based Model Checking,” in Proceedings of the Computer Aided Verification, Berlin Heidelberg, Germany, pp. 1-13, 2003.

[21] Moura L. and Bjørner N., “Z3: An Efficient SMT Solver,” in Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Budapest, pp. 337-340, 2008.

[22] Sharma R., Gupta S., Hariharan B., Aiken A., Liang P., and Nori A., “A Data Driven Approach for Algebraic Loop Invariants,” in Proceedings of European Conference on Programming Languages and Systems, Rome, pp. 574-592, 2013.

[23] Sharma R., “From Invariant Checking to Invariant Inference Using Randomized Search,” in Proceedings of Computer Aided Verification, Vienna, pp. 88-105, 2014.

[24] Sharma R., “Interpolants as Classifiers,” in Proceedings of International Conference on Computer Aided Verification, Berlin, pp. 71-87, 2012.

[25] Sharma R. and Aiken A., “Verification as Learning Geometric Concepts,” in Proceedings of International Static Analysis Symposium, Seattle, pp. 388-411, 2013.

[26] Stavnycha M., Yin H., and Römer T., “A Large- Scale Survey on the Effects of Selected Development Practices on Software Correctness,” in Proceedings of International Conference on Software and System Process, Korea, pp. 117-121, 2015.

[27] Uqaili I. and Ahsan S., “Machine Learning Based Prediction of Complex Bugs in Source Code,” The International Arab Journal of Information Technology, vol. 17, no. 1, pp. 26- 37, 2020.

[28] Vizel Y., Gurfinkel A., Shoham S., and Malik S., “IC3 - Flipping the E in ICE,” in Proceedings of International Conference on Verification, Model Checking and Abstract Interpretation, Paris, pp. 521-538, 2017. 856 The International Arab Journal of Information Technology, Vol. 17, No. 6, November 2020 Shengbing Ren was born on August 4, 1969 at Yueyang City, Hunan Province, China. He received his Bachelor of Science degree in Computer Software from Department of Mathematics, Huazhong Normal University, Hubei Province, China in 1992. He received his Master’s degree in Computer Application Technology in 1995 from Department of Computer, Central South University of Technology, Hunan Province, China. He received his Doctor’s degree in Control Theory and Control Engineering in 2007 from School of Information Science and Engineering, Central South University, Hunan Province, China. His research interests include: software engineering, embedded system, image processing, pattern recognition, dependable software. He is a professor in School of Computer Science and Engineering, Central South University, China. He is a Senior Member of China Computer Federation. He accomplished 11 research projects including 2 the National Natural Science Foundation of China as a key member, and over 60 papers was published. Now, he is dedicated to the research concentrated mostly on dependable software and pattern recognition. Xiang Zhang was born on April19, 1993 at Anqing City, Anhui Province, China. He received his Bachelor of Science degree in communication engineering, Central South University of forestry science and technology University, Hunan Province, China in 2015. He received his Master’s degree in software engineering, Central South University of Technology, Hunan Province, Chinain 2019.His research interests include: software engineering, machine learning. He is a student in School of Computer Science and Engineering, Central South University, China.