Assertion Recommendation for Formal Program Verification

Formal program verification is a powerful technique to ensure the correctness of programs. To perform this technique, one oftentimes needs to manually specify assertions, which is a time-consuming and error-prone task. Generating assertions automatically can significantly improve the usability of formal program verification. To decide where an assertion is needed heavily and which value range of the variable should be checked are the most challenging parts of assertion recommendation. This paper proposes the first assertion recommendation approach for program verification. With the help of machine learning techniques, the approach automatically decides whether a program function needs to add assertions. If an assertion is needed, the approach automatically recommends a variable that is most likely to occur in this assertion. Meanwhile, a value range of the variable is suggested. Our method of assertion recommendation has been integrated into Ceagle Online (a program verifier) and evaluated on the benchmarks of SV-COMP and CProver. Our best performance in assertion necessity classification can reach 92.1192% accuracy rate, 84.2281% precision rate and 86.8512% recall rate.