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