Quantifier instantiation techniques for finite model finding in SMT

DOI10.1007/978-3-642-38574-2_26MaRDI QIDQ4928453zbMATH OpenOpenAlexFDO

Authors Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstić, Morgan Deters, Clark Barrett

Publication date 14 June 2013

Published in Automated Deduction – CADE-24 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-38574-2_26

Mathematics Subject Classification ID

Recommendations

• Constraint solving for finite model finding in SMT solvers
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Syntax-guided quantifier instantiation
• Solving quantified verification conditions using satisfiability modulo theories
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories

Cited in

(29)

• A unifying splitting framework
• Verifying Whiley programs with Boogie
• Syntax-guided quantifier instantiation
• Incremental search for conflict and unit instances of quantified formulas with E-matching
• Refutation-based synthesis in SMT
• Finite model finding using the logic of equality with uninterpreted functions
• Extending SMT solvers to higher-order logic
• Revisiting enumerative instantiation
• A decision procedure for (co)datatypes in SMT solvers
• Automated reasoning with restricted intensional sets
• On the key dependent message security of the Fujisaki-Okamoto constructions
• Fault-tolerant aggregate signatures
• Model finding for recursive functions in SMT
• Decision procedures for flat array properties
• Satisfiability modulo theories
• Bounded quantifier instantiation for checking inductive invariants
• Congruence closure with free variables
• A decision procedure for (co)datatypes in SMT solvers
• Efficient E-Matching for SMT Solvers
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Constraint solving for finite model finding in SMT solvers
• Model generation for quantified formulas: a taint-based approach
• Early verification of legal compliance via bounded satisfiability checking
• SMT and functional equation solving over the reals: challenges from the IMO
• Machine learning for quantifier selection in cvc5
• Bounded satisfiability checking of \(\mathrm{FOL}^*\) formulas with aggregations
• The QSMA algorithm for quantifiers in SMT
• Verifying SQL queries using theories of tables and relations
• Experiments on infinite model finding in SMT solving

Describes a project that uses

Uses Software

• iProver

This page was built for publication: Quantifier instantiation techniques for finite model finding in SMT

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