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