Latticed Craig Interpolation with an Application to Probabilistic Verification


In this work, we are primarily concerned with the question: Is Craig interpolation applicable to the automatic, quantitative verification of (infinite-state) probabilistic programs with potentially unbounded loops? Our preliminary results indicate an affirmative answer:

  • Quantitative Craig interpolants. We propose a quantitative version of Craig interpolants by extending predicates to expectations (expected values), which can be used to discover quantitative loop invariants that suffice to establish upper bounds on the least fixed point;
  • Latticed Craig interpolation. We present latticed Craig interpolation by exploiting quantitative interpolants over complete lattices, which conservatively extends both McMillan’s interpolation-based SAT model checking (to the quantitative setting) and Batz et al.’s latticed bounded model checking (to the unbounded case);
  • Soundness and Completeness. We show that our latticed interpolation procedure is sound and establish sufficient conditions under which it is further complete.
  • Synthesizing quantitative interpolants. We (semi-)automated our verification procedure by employing a counterexample-guided inductive synthesis framework to automatically generate quantitative interpolants. Our implementation shows promise: It finds invariants for non-trivial infinite-state programs with unbounded loops.

In CIBD 2024
Mingqi Yang
Mingqi Yang
Ph.D. Candidate

My research interests include formal verification, programming theory, and mathematical aspects of computer science.

Mingshuai Chen
Mingshuai Chen
ZJU100 Young Professor

My research interests include formal verification, programming theory, and logical aspects of computer science.

Zhiang Wu
Zhiang Wu

My research interest lies in formal verification of probabilistic programs by synthesizing inductive invariants as Craig interpolants.