Yotam M. Y. Feldman ; Oded Padon ; Neil Immerman ; Mooly Sagiv ; Sharon Shoham - Bounded Quantifier Instantiation for Checking Inductive Invariants

lmcs:4018 - Logical Methods in Computer Science, August 21, 2019, Volume 15, Issue 3 - https://doi.org/10.23638/LMCS-15(3:18)2019
Bounded Quantifier Instantiation for Checking Inductive InvariantsArticle

Authors: Yotam M. Y. Feldman ORCID; Oded Padon ; Neil Immerman ; Mooly Sagiv ; Sharon Shoham ORCID

    We consider the problem of checking whether a proposed invariant $\varphi$ expressed in first-order logic with quantifier alternation is inductive, i.e. preserved by a piece of code. While the problem is undecidable, modern SMT solvers can sometimes solve it automatically. However, they employ powerful quantifier instantiation methods that may diverge, especially when $\varphi$ is not preserved. A notable difficulty arises due to counterexamples of infinite size. This paper studies Bounded-Horizon instantiation, a natural method for guaranteeing the termination of SMT solvers. The method bounds the depth of terms used in the quantifier instantiation process. We show that this method is surprisingly powerful for checking quantified invariants in uninterpreted domains. Furthermore, by producing partial models it can help the user diagnose the case when $\varphi$ is not inductive, especially when the underlying reason is the existence of infinite counterexamples. Our main technical result is that Bounded-Horizon is at least as powerful as instrumentation, which is a manual method to guarantee convergence of the solver by modifying the program so that it admits a purely universal invariant. We show that with a bound of 1 we can simulate a natural class of instrumentations, without the need to modify the code and in a fully automatic way. We also report on a prototype implementation on top of Z3, which we used to verify several examples by Bounded-Horizon of bound 1.


    Volume: Volume 15, Issue 3
    Published on: August 21, 2019
    Accepted on: June 12, 2019
    Submitted on: October 26, 2017
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages
    Funding:
      Source : OpenAIRE Graph
    • Verifying and Synthesizing Software Compositions; Funder: European Commission; Code: 321174
    • Supervised Verification of Infinite-State Systems; Funder: European Commission; Code: 759102

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1092 times.
    This article's PDF has been downloaded 252 times.