An Invariant Inference Framework by Active Learning and SVMs

We introduce a fast invariant inference framework based on active learning and SVMs (Support Vector Machines) which aims to systematically generate a variety of loop invariants efficiently. Given a program containing one loop along with a precondition and a post-condition, our approach can learn an invariant which is sufficiently strong for program verification or otherwise provide counter-examples to assist software developers to locate program bugs. By invoking learning and checking phases iteratively, our preliminary experiments show, this approach may be potentially more effective and efficient when compared with other existing approaches.