swMATH7736MaRDI QIDQ19753FDOQ19753
Author name not available (Why is that?)
Official website: https://github.com/danr/hipspec
Source code repository: https://github.com/danr/hipspec
Cited In (40)
- Equivalence checking of two functional programs using inductive theorem provers
- Disproving inductive entailments in separation logic via base pair approximation
- IsaCoSy
- 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
- CIRC
- QuickCheck
- Zeno
- Leon
- HERMIT
- HR
- Hipster
- Cyclist
- Graphsc
- Pirate
- QuickSpec
- InKa
- TIP
- Angelic Verification
- MATHsAiD
- QuodLibet
- Refal
- Coinductive
- AVATAR
- Slide
- TRANSIT
- Imandra
- Theory exploration powered by deductive synthesis
- Unprovability results for clause set cycles
- TIP: tools for inductive provers
- Clause set cycles and induction
- Hipster: integrating theory exploration in a proof assistant
- Induction and Skolemization in saturation theorem proving
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Quick specifications for the busy programmer
- Combining induction and saturation-based theorem proving
- Inductive theorem proving based on tree grammars
This page was built for software: HipSpec
