Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas

DOI10.1007/978-3-642-18070-5_6zbMath1308.68039OpenAlexW1579447681MaRDI QIDQ3067537

Christoph D. Gladisch

Publication date: 21 January 2011

Published in: Formal Verification of Object-Oriented Software (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-18070-5_6

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Yices
• cvc3
• z3
• SIMPLIFY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Solving quantified verification conditions using satisfiability modulo theories
• Automated model building
• E-matching for Fun and Profit
• Simplify: a theorem prover for program checking
• Efficient E-Matching for SMT Solvers
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Quantifier Elimination and Provers Integration
• Sequential, Parallel, and Quantified Updates of First-Order Structures
• Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
• Challenges in Satisfiability Modulo Theories
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas