Efficiently Learning Safety Proofs from Appearance as well as Behaviours

摘要

Proving safety of programs relies principally on discovering invariants that are inductive and adequate. Obtaining such invariants, therefore, has been studied widely from diverse perspectives, including even mining them from the input program's source in a guess-and-check manner [13]. However, guessing candidates based on syntactical constructions of the source code has its limitations. For one, a required invariant may not manifest on the syntactic surface of the program. Secondly, a poor guess may give rise to a series of expensive checks. Furthermore, unlike conjunctions, refining disjunctive invariant candidates is unobvi-ous and may frequently cause the proof search to diverge. This paper attempts to overcome these limitations, by learning from both - appearance and behaviours of a program. We present an algorithm that (ⅰ) infers useful invariants by observing a program's syntactic source as well as its semantics, and (ⅱ) looks for conditional invariants, in the form of implications, that are guided by counterexamples to inductiveness. Our experiments demonstrate its benefits on several benchmarks taken from SV-COMP and the literature.