Solving quantified verification conditions using satisfiability modulo theories

DOI10.1007/s10472-009-9153-6zbMath1184.68461OpenAlexW2009715851MaRDI QIDQ1037401

Cesare Tinelli, Clark Barrett, Yeting Ge

Publication date: 16 November 2009

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-009-9153-6

zbMATH Keywords

first-order automated theorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items

Constraint solving for finite model finding in SMT solvers ⋮ Verification of SMT systems with quantifiers ⋮ 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 ⋮ An interleaved depth-first search method for the linear optimization problem with disjunctive constraints ⋮ Sharpening constraint programming approaches for bit-vector theory ⋮ Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas

Uses Software

• VAMPIRE
• SMT-LIB
• SPASS
• TPTP
• SPASS+T
• cvc3
• z3
• SIMPLIFY
• ESC/Java

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The TPTP problem library. CNF release v1. 2. 1
• Ordered semantic hyper-linking
• Partial instantiation methods for inference in first-order logic
• Automated deduction by theory resolution
• The model evolution calculus as a first-order DPLL method
• E-matching for Fun and Profit
• Simplify: a theorem prover for program checking
• Efficient E-Matching for SMT Solvers
• Automated Reasoning
• Computer Aided Verification
• Splitting on Demand in SAT Modulo Theories