Satisfiability solving and model generation for quantified first-order logic formulas

DOI10.1007/978-3-642-18070-5_6MaRDI QIDQ3067537zbMATH OpenOpenAlexFDO

Authors 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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model generation for quantified formulas: a taint-based approach
• scientific article; zbMATH DE number 2219519
• Solving quantified verification conditions using satisfiability modulo theories
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Constraint solving for finite model finding in SMT solvers

Cites work

• Automated model building
• Challenges in Satisfiability Modulo Theories
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• E-matching for fun and profit
• Efficient E-Matching for SMT Solvers
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 2080299 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 1765699 (Why is no real title available?)
• Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
• Quantifier Elimination and Provers Integration
• Sequential, Parallel, and Quantified Updates of First-Order Structures
• Simplify: a theorem prover for program checking
• Solving quantified verification conditions using satisfiability modulo theories
• Verification, Model Checking, and Abstract Interpretation

Cited in

(5)

• A full first-order constraint solver for decomposable theories
• Presenting Herbrand models with linguistically motivated techniques
• scientific article; zbMATH DE number 2165692 (Why is no real title available?)
• scientific article; zbMATH DE number 2219519 (Why is no real title available?)
• Model generation for quantified formulas: a taint-based approach

Describes a project that uses

Uses Software

• cvc3
• z3
• Yices
• SIMPLIFY

This page was built for publication: Satisfiability solving and model generation for quantified first-order logic formulas

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