Quantifier Instantiation Techniques for Finite Model Finding in SMT
From MaRDI portal
Publication:4928453
DOI10.1007/978-3-642-38574-2_26zbMath1381.68275OpenAlexW2098095758MaRDI QIDQ4928453
Amit Goel, Andrew Reynolds, Morgan Deters, Clark Barrett, Sava Krstić, Cesare Tinelli
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
Related Items
A decision procedure for (co)datatypes in SMT solvers, Decision procedures for flat array properties, Satisfiability Modulo Theories, A Decision Procedure for (Co)datatypes in SMT Solvers, Automated reasoning with restricted intensional sets, Syntax-guided quantifier instantiation, Bounded Quantifier Instantiation for Checking Inductive Invariants, Congruence Closure with Free Variables, Refutation-based synthesis in SMT, On the Key Dependent Message Security of the Fujisaki-Okamoto Constructions, Fault-Tolerant Aggregate Signatures, Model Finding for Recursive Functions in SMT, A unifying splitting framework, Extending SMT solvers to higher-order logic, Verifying Whiley programs with Boogie
Uses Software
