Synthesizing conjunctive and disjunctive linear invariants by K-means++ and SVM
المؤلفون المشاركون
المصدر
The International Arab Journal of Information Technology
العدد
المجلد 17، العدد 6 (30 نوفمبر/تشرين الثاني 2020)، ص ص. 847-856، 10ص.
الناشر
جامعة الزرقاء عمادة البحث العلمي
تاريخ النشر
2020-11-30
دولة النشر
الأردن
عدد الصفحات
10
التخصصات الرئيسية
تكنولوجيا المعلومات وعلم الحاسوب
الملخص EN
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.
نمط استشهاد جمعية علماء النفس الأمريكية (APA)
Ren, Shengbing& Zhang, Xiang. 2020. Synthesizing conjunctive and disjunctive linear invariants by K-means++ and SVM. The International Arab Journal of Information Technology،Vol. 17, no. 6, pp.847-856.
https://search.emarefa.net/detail/BIM-1432401
نمط استشهاد الجمعية الأمريكية للغات الحديثة (MLA)
Ren, Shengbing& Zhang, Xiang. Synthesizing conjunctive and disjunctive linear invariants by K-means++ and SVM. The International Arab Journal of Information Technology Vol. 17, no. 6 (Nov. 2020), pp.847-856.
https://search.emarefa.net/detail/BIM-1432401
نمط استشهاد الجمعية الطبية الأمريكية (AMA)
Ren, Shengbing& Zhang, Xiang. Synthesizing conjunctive and disjunctive linear invariants by K-means++ and SVM. The International Arab Journal of Information Technology. 2020. Vol. 17, no. 6, pp.847-856.
https://search.emarefa.net/detail/BIM-1432401
نوع البيانات
مقالات
لغة النص
الإنجليزية
الملاحظات
Includes bibliographical references : p. 854-855
رقم السجل
BIM-1432401
قاعدة معامل التأثير والاستشهادات المرجعية العربي "ارسيف Arcif"
أضخم قاعدة بيانات عربية للاستشهادات المرجعية للمجلات العلمية المحكمة الصادرة في العالم العربي
تقوم هذه الخدمة بالتحقق من التشابه أو الانتحال في الأبحاث والمقالات العلمية والأطروحات الجامعية والكتب والأبحاث باللغة العربية، وتحديد درجة التشابه أو أصالة الأعمال البحثية وحماية ملكيتها الفكرية. تعرف اكثر