Bounded quantifier instantiation for checking inductive invariants

DOI10.1007/978-3-662-54577-5_5MaRDI QIDQ3303891zbMATH OpenOpenAlexFDO

Authors Yotam M. Y. Feldman, Oded Padon, Mooly Sagiv, Sharon Shoham, Neil Immerman

Publication date 5 August 2020

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1710.08668

zbMATH Keywords

existential quantifierfirst-order logic with quantifier alternationprogram verificationuniversal quantifierverification condition

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: 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.

Recommendations

• Bounded quantifier instantiation for checking inductive invariants
• Verification of SMT systems with quantifiers
• Induction for SMT solvers
• Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
• Quantifiers on demand

Cites work

• All for the price of few (parameterized verification through view abstraction)
• An improved algorithm for decentralized extrema-finding in circular configurations of processes
• Back to the future, revisiting precise program verification using SMT solvers
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Computer Science Logic
• Dafny: an automatic program verifier for functional correctness
• Deciding local theory extensions via E-matching
• scientific article; zbMATH DE number 1617328 (Why is no real title available?)
• scientific article; zbMATH DE number 1956566 (Why is no real title available?)
• scientific article; zbMATH DE number 965572 (Why is no real title available?)
• Ivy
• Loosely guarded fragment of first-order logic has the finite model property
• On Local Reasoning in Verification
• Property-directed inference of universal invariants or proving their absence
• Quantifier instantiation techniques for finite model finding in SMT
• Simplify: a theorem prover for program checking
• Solving quantified verification conditions using satisfiability modulo theories
• Verifying properties of well-founded linked lists
• View abstraction -- a tutorial (invited paper)

Cited in

(7)

• scientific article; zbMATH DE number 1629964 (Why is no real title available?)
• Identification through Inductive Verification
• Deciding the Inductive Validity of ∀ ∃ * Queries
• Bounded quantifier instantiation for checking inductive invariants
• Verification of SMT systems with quantifiers
• Inferring invariants with quantifier alternations: taming the search space explosion
• Counterexample-guided partial bounding for recursive function synthesis

Describes a project that uses

Uses Software

• Dafny
• z3
• SIMPLIFY
• MONA
• ESC/Java
• TVLA
• Ivy
• VeriCon
• Ivy
• IronFleet

This page was built for publication: Bounded quantifier instantiation for checking inductive invariants

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3303891)