Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
From MaRDI portal
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60) Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25)
Recommendations
- Quantifier instantiation techniques for finite model finding in SMT
- Solving quantified verification conditions using satisfiability modulo theories
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- An instantiation scheme for satisfiability modulo theories
- Syntax-guided quantifier instantiation
Cited in
(67)- A learning-based approach to synthesizing invariants for incomplete verification engines
- The QSMA algorithm for quantifiers in SMT
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Verifying Whiley programs with Boogie
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Not all bugs are created equal, but robust reachability can tell the difference
- Quantifier simplification by unification in SMT
- Incremental Instance Generation in Local Reasoning
- Contract-based verification of MATLAB-style matrix programs
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Schemata of SMT-problems
- Alloy*: a general-purpose higher-order relational constraint solver
- Inner and outer approximate quantifier elimination for general reachability problems
- Deductive verification of floating-point Java programs in KeY
- Syntax-guided quantifier instantiation
- Incremental search for conflict and unit instances of quantified formulas with E-matching
- On solving quantified bit-vector constraints using invertibility conditions
- Automatically inferring loop invariants via algorithmic learning
- Decision procedures for flat array properties
- Interpolation systems for ground proofs in automated deduction: a survey
- Adding decision procedures to SMT solvers using axioms with triggers
- A solver for arrays with concatenation
- Array theory of bounded elements and its applications
- Fault-tolerant aggregate signatures
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- An instantiation scheme for satisfiability modulo theories
- An extension of lazy abstraction with interpolation for programs with arrays
- Bounded quantifier instantiation for checking inductive invariants
- Congruence closure with free variables
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
- Experiments on infinite model finding in SMT solving
- Fuzzy answer set computation via satisfiability modulo theories
- Refutation-based synthesis in SMT
- Revisiting enumerative instantiation
- Solving quantified verification conditions using satisfiability modulo theories
- A formal model to prove instantiation termination for E-matching-based axiomatisations
- First-order automatic literal model generation
- Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
- Efficiently solving quantified bit-vector formulas
- Unifying splitting
- Cardinality constraints for arrays (decidability results and applications)
- Bugs, moles and skeletons: symbolic reasoning for software development
- Quantifier instantiation techniques for finite model finding in SMT
- Satisfiability modulo theories
- Modular instantiation schemes
- Temporal prophecy for proving temporal properties of infinite-state systems
- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
- An approximation framework for solvers and decision procedures
- Solving hard Mizar problems with instantiation and strategy invention
- Invariant neural architecture for learning term synthesis in instantiation proving
- Extending SMT solvers to higher-order logic
- On interpolation in automated theorem proving
- A decision procedure for (co)datatypes in SMT solvers
- CoReS: a tool for computing core graphs via SAT/SMT solvers
- Solving quantified linear arithmetic by counterexample-guided instantiation
- A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers
- Satisfiability solving and model generation for quantified first-order logic formulas
- Model finding for recursive functions in SMT
- Automated reasoning with restricted intensional sets
- A unifying splitting framework
- Counterexample-Guided Model Synthesis
- Towards Complete Reasoning about Axiomatic Specifications
- Bitwuzla
- Early verification of legal compliance via bounded satisfiability checking
- Non-classical logics in satisfiability modulo theories
- MedleySolver: online SMT algorithm selection
- Constraint solving for finite model finding in SMT solvers
This page was built for publication: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3636870)
