HipSpec
From MaRDI portal
Cited in
(41)- IsaPlanner
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- Superposition with structural induction
- CIRC
- QuickCheck
- Zeno
- Unprovability results for clause set cycles
- Induction and Skolemization in saturation theorem proving
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Leon
- HERMIT
- HR
- Combining induction and saturation-based theorem proving
- Hipster
- Inductive theorem proving based on tree grammars
- Equivalence checking of two functional programs using inductive theorem provers
- Proving properties of functional programs by equality saturation
- Cyclist
- TIP
- Graphsc
- QuickSpec
- Pirate
- InKa
- MATHsAiD
- Angelic Verification
- TIP: tons of inductive problems
- Disproving inductive entailments in separation logic via base pair approximation
- TIP: tools for inductive provers
- QuodLibet
- Refal
- Coinductive
- Slide
- AVATAR
- TRANSIT
- Automating Inductive Proofs Using Theory Exploration
- Clause set cycles and induction
- Imandra
- Quick specifications for the busy programmer
- Hipster: integrating theory exploration in a proof assistant
- IsaCoSy
- Theory exploration powered by deductive synthesis
This page was built for software: HipSpec
