Collaborative Inference of Combined Invariants
Program verification techniques can be split into two groups: white-box (like CEGAR, IC3/PDR) and black-box "guess and check" (like ICE, CEGIS, FMF). On the one hand, white-box approaches heavily depend on generalization strategy (e.g., interpolation strength) and the structure of the verified system. On the other hand, black-box learning approaches are tied to the shape of examples from which they learn. In this talk, we will discuss how to obtain a collaborative invariant inference by integrating white-box and black-box approaches. The proposed technique not only combines their pros and mitigates their cons but also allows one to infer rich combined invariants. Their expressiveness is the main reason why the presented technique is also capable of proving the safety of more programs than just an independent run of combined approaches could. We instantiate our technique for one white-box (PDR in SPACER engine in Z3) and one black-box approach (tree automata learning by finite-model finding in RInGen) in the task of proving the safety of programs over algebraic datatypes. Our second instantiation uses the Vampire theorem prover as a black-box invariant "learner" - this shows the flexibility of our technique. Our implementation increased the number of verified programs by Vampire by 30% and by RInGen by 250%.
Speaker: Yurii Kostyukov
Google Meet: https://meet.google.com/myu-dhmz-gvu