Exploring theories with a model-finding assistant

DOI10.1007/978-3-319-21401-6_30MaRDI QIDQ3454114zbMATH OpenOpenAlexFDO

Authors Salman Saghafi, Ryan Danas, Daniel J. Dougherty

Publication date 2 December 2015

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

Full work available at URL https://doi.org/10.1007/978-3-319-21401-6_30

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• CompoSAT: specification-guided coverage for model finding
• Proving semantic properties as first-order satisfiability
• Model generation for quantified formulas: a taint-based approach
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Satisfiability modulo bounded checking

Cites work

• A Proof Procedure for Data Dependencies
• A tableau calculus for minimal model reasoning
• Automating Coherent Logic
• Blocking and Other Enhancements for Bottom-Up Model Generation Methods
• Computing finite models by reduction to function-free clause logic
• Domain theory in logical form
• First order categorical logic. Model-theoretical methods in the theory of topoi and related categories
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• scientific article; zbMATH DE number 1301750 (Why is no real title available?)
• scientific article; zbMATH DE number 1953133 (Why is no real title available?)
• scientific article; zbMATH DE number 860049 (Why is no real title available?)
• iProver-Eq: An Instantiation-Based Theorem Prover with Equality
• Kodkod: A Relational Model Finder
• Positive unit hyperresolution tableaux and their application to minimal model generation
• Searching for Shapes in Cryptographic Protocols
• Sheaves and geometric logic and applications to modular verification of complex systems
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• XML queries and constraints, containment and reformulation

Cited in

(4)

• CompoSAT: specification-guided coverage for model finding
• Pardinus: a temporal relational model finder
• Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA
• Theory exploration powered by deductive synthesis

Describes a project that uses

Uses Software

• MiniSat
• TPTP
• Darwin
• z3
• E-Darvin
• Mace4
• Kodkod
• iProver-Eq
• iProver
• Razor

This page was built for publication: Exploring theories with a model-finding assistant

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