Synthesizing
Conjunctive and Disjunctive Linear Invariants by K-means++ and SVM
Shengbing Ren and
Xiang Zhang
School of Computer
Science and Engineering, Central South University, China
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.
Keywords: Software verification,
conjunctive invariant, disjunctive invariant, k-means++, SVM.
Received September 5, 2018; accepted January 28,
2020