scholarly journals Foundations for natural proofs and quantifier instantiation

2018 ◽  
Vol 2 (POPL) ◽  
pp. 1-30 ◽  
Author(s):  
Christof Löding ◽  
P. Madhusudan ◽  
Lucas Peña
Keyword(s):  
Quantifier Instantiation

scholarly journals Counterexample-Guided Quantifier Instantiation for Synthesis in SMT

2015 ◽  
pp. 198-216 ◽  
Author(s):  
Andrew Reynolds ◽  
Morgan Deters ◽  
Viktor Kuncak ◽  
Cesare Tinelli ◽  
Clark Barrett
Keyword(s):  
Quantifier Instantiation

scholarly journals Complete decision procedure for the theory of bounded pointer arithmetic based on quantifier instantiation and SMT

2021 ◽  
Vol 33 (4) ◽  
pp. 177-194
Author(s):  
Rafael Faritovich Sadykov ◽  
Mikhail Usamovich Mandrykin
Keyword(s):  
Program Verification ◽  
Source Code ◽  
Decision Procedures ◽  
C Programs ◽  
Smt Solver ◽  
Smt Solvers ◽  
Relevant Logics ◽  
Soundness And Completeness ◽  
C Program ◽  
Quantifier Instantiation

The process of developing C programs is quite often prone to errors related to the uses of pointer arithmetic and operations on memory addresses. This promotes a need in developing various tools for automated program verification. One of the techniques frequently employed by those tools is invocation of appropriate decision procedures implemented within existing SMT-solvers. But at the same time both the SMT standard and most existing SMT-solvers lack the relevant logics (combinations of logical theories) for directly and precisely modelling the semantics of pointer operations in C. One of the possible ways to support these logics is to implement them in an SMT solver, but this approach can be time-consuming (as requires modifying the solver’s source code), inflexible (introducing any changes to the theory’s signature or semantics can be unreasonably hard) and limited (every solver has to be supported separately). Another way is to design and implement custom quantifier instantiation strategies. These strategies can be then used to translate formulas in the desired theory combinations to formulas in well-supported decidable logics such as QF_UFLIA. In this paper, we present an instantiation procedure for translating formulas in the theory of bounded pointer arithmetic into the QF_UFLIA logic. We formally proved soundness and completeness of our instantiation procedure in Isabelle/HOL. The paper presents an informal description of this proof of the proposed procedure. The theory of bounded pointer arithmetic itself was formulated based on known errors regarding the correct use of pointer arithmetic operations in industrial code as well as the semantics of these operations specified in the C standard. Similar procedure can also be defined for a practically relevant fragment of the theory of bit vectors (monotone propositional combinations of equalities between bitwise expressions). Our approach is sufficient to obtain efficient decision procedures implemented as Isabelle/HOL proof methods for several decidable logical theories used in C program verification by relying on the existing capabilities of well-known SMT solvers, such as Z3 and proof reconstruction capabilities of the Isabelle/HOL proof assistant.

scholarly journals Syntax-Guided Quantifier Instantiation

2021 ◽  
pp. 145-163
Author(s):  
Aina Niemetz ◽  
Mathias Preiner ◽  
Andrew Reynolds ◽  
Clark Barrett ◽  
Cesare Tinelli
Keyword(s):  
State Of The Art ◽  
Satisfiability Modulo Theories ◽  
Floating Point ◽  
New Approach ◽  
Smt Solver ◽  
Floating Point Arithmetic ◽  
Novel Approach ◽  
Non Linear ◽  
Quantifier Instantiation ◽  
Point Arithmetic

AbstractThis paper presents a novel approach for quantifier instantiation in Satisfiability Modulo Theories (SMT) that leverages syntax-guided synthesis (SyGuS) to choose instantiation terms. It targets quantified constraints over background theories such as (non)linear integer, reals and floating-point arithmetic, bit-vectors, and their combinations. Unlike previous approaches for quantifier instantiation in these domains which rely on theory-specific strategies, the new approach can be applied to any (combined) theory, when provided with a grammar for instantiation terms for all sorts in the theory. We implement syntax-guided instantiation in the SMT solver CVC4, leveraging its support for enumerative SyGuS. Our experiments demonstrate the versatility of the approach, showing that it is competitive with or exceeds the performance of state-of-the-art solvers on a range of background theories.

scholarly journals Conflicts, Models and Heuristics for Quantifier Instantiation in SMT

10.29007/jmd3 ◽  
2018 ◽  
Author(s):  
Andrew Reynolds
Keyword(s):  
Formal Methods ◽  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Software Verification ◽  
Satisfiability Modulo Theories ◽  
Smt Solvers ◽  
Recent Advances ◽  
Common Technique ◽  
Quantifier Instantiation ◽  
Future Work

Satisfiability Modulo Theories (SMT) solvers have emerged as prominent tools in formal methods applications. While originally targeted towards quantifier-free inputs, SMT solvers are now often used for handling quantified formulas in automated theorem proving and software verification applications. The most common technique for handling quantified formulas in modern SMT solvers in quantifier instantiation. This paper gives an overview of recent advances in quantifier instantiation in SMT. In addition to the well-known technique known as E-matching, we discuss the use of conflicts and models for accelerating the search for (un)satisfiably. We further mention new instantiation-based techniques that are specialized to background theories such as linear real and integer arithmetic, and future work in this direction.

Quantifier Instantiation Techniques for Finite Model Finding in SMT

2013 ◽  
pp. 377-391 ◽  
Author(s):  
Andrew Reynolds ◽  
Cesare Tinelli ◽  
Amit Goel ◽  
Sava Krstić ◽  
Morgan Deters ◽  
...  
Keyword(s):  
Finite Model ◽  
Model Finding ◽  
Quantifier Instantiation

scholarly journals A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories

10.29007/b923 ◽  
2018 ◽  
Author(s):  
Joshua Bax
Keyword(s):  
Theorem Proving ◽  
Partial Function ◽  
Simplifying Assumptions ◽  
Model Finding ◽  
Free Function ◽  
Quantifier Instantiation ◽  
Superposition Calculus

Generalised Model Finding (GMF) is a quantifier instantiation heuristic for the superposition calculus in the presence of interpreted theories with arbitrarily quantified free function symbols ranging into theory sorts.The free function symbols are approximated by finite partial function graphs along with some simplifying assumptions which are iteratively refined.Here we present an outline of the GMF approach, give an improvementthat addresses some of these and then present someideas for extending it with concepts from instantiation based theorem proving.

Sign in / Sign up

Export Citation Format

Share Document