Bounded Quantifier Instantiation for Checking Inductive Invariants

DOI10.1007/978-3-662-54577-5_5zbMath1452.68119arXiv1710.08668OpenAlexW2598582440MaRDI QIDQ3303891

Oded Padon, Sharon Shoham, Mooly Sagiv, Yotam M. Y. Feldman, 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

program verificationexistential quantifieruniversal quantifierverification conditionfirst-order logic with quantifier alternation

Mathematics Subject Classification ID

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

Related Items

Counterexample-guided partial bounding for recursive function synthesis

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Solving quantified verification conditions using satisfiability modulo theories
• Loosely guarded fragment of first-order logic has the finite model property
• Deciding local theory extensions via E-matching
• Property-directed inference of universal invariants or proving their absence
• All for the Price of Few
• Dafny: An Automatic Program Verifier for Functional Correctness
• Back to the future
• Simplify: a theorem prover for program checking
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• An improved algorithm for decentralized extrema-finding in circular configurations of processes
• Quantifier Instantiation Techniques for Finite Model Finding in SMT
• Computer Science Logic
• Verifying properties of well-founded linked lists
• On Local Reasoning in Verification
• Ivy