Bounded model generation for Isabelle/HOL

MaRDI QIDQ2848061zbMATH OpenFDO

Authors Tjark Weber

Publication date 25 September 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066105050759

Mathematics Subject Classification ID

Recommendations

• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Satisfiability modulo bounded checking
• Automatic proof and disproof in Isabelle/HOL
• scientific article; zbMATH DE number 2219519
• Reducing higher-order theorem proving to a sequence of SAT problems

Cited in

(5)

• Satisfiability modulo bounded checking
• Formal Proof: Reconciling Correctness and Understanding
• Generating counterexamples for structural inductions by exploiting nonstandard models
• scientific article; zbMATH DE number 2219519 (Why is no real title available?)
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Bounded model generation for Isabelle/HOL

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