Model Finding for Recursive Functions in SMT
From MaRDI portal
Publication:2817915
DOI10.1007/978-3-319-40229-1_10zbMath1475.68448OpenAlexW2468404022MaRDI QIDQ2817915
Andrew Reynolds, Cesare Tinelli, Simon Cruanes, Jasmin Christian Blanchette
Publication date: 5 September 2016
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01336082/file/conf.pdf
Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
A decision procedure for (co)datatypes in SMT solvers, Nunchaku, Satisfiability and synthesis modulo oracles, Alloy*: a general-purpose higher-order relational constraint solver, Model Finding for Recursive Functions in SMT
Uses Software
Cites Work
- Monotonicity inference for higher-order formulas
- Automated flaw detection in algebraic specifications
- Computing finite models by reduction to function-free clause logic
- Extending Sledgehammer with SMT solvers
- Model Finding for Recursive Functions in SMT
- Non-cyclic Sorts for First-Order Satisfiability
- Proving Infinite Satisfiability
- Foundational extensible corecursion: a proof assistant perspective
- A Decision Procedure for (Co)datatypes in SMT Solvers
- Efficient E-Matching for SMT Solvers
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Institutions: abstract model theory for specification and programming
- Quantifier Instantiation Techniques for Finite Model Finding in SMT
- Sort It Out with Monotonicity
- Productive coprogramming with guarded recursion
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
- Case-Analysis for Rippling and Inductive Proof
- Kodkod: A Relational Model Finder
