On Template-Based Inference of Rich Invariants in Leon
Ravichandhran Madhavan, Viktor Kunčak · 2013
We present an approach for inferring rich invariants involv-ing user-defined recursive functions over numerical and al-gebraic data types. In our approach, the developer provides the desired shape of the invariant using a set of templates. The templates are quantifier-free affine predicates with un-known coefficients. We also provide an enumeration based strategy for automatically inferring some of the templates. We present a scalable counter-example driven algorithm that finds the unknown coefficients in templates and thus computes expressive inductive invariants. Our algorithm in-crementally solves a set of quantified constraints involv-ing recursive functions and data structures. We discuss sev-eral optimizations that make the approach scale to complex programs and present an empirical evaluation. Our imple-mentation proves correctness properties as well as symbolic bounds on running times of recursive programs. For exam-ple, the implementation establishes that the time taken to insert into a red-black tree is bounded by the logarithm of its size. 1.