swMATH44476MaRDI QIDQ5973367FDOQ5973367
Author name not available (Why is that?)
Official website: https://www.cse.chalmers.se/~jomoa/papers/ConjSynthesisJAR2011.pdf
Cited In (26)
- Equivalence checking of two functional programs using inductive theorem provers
- Algorithmic introduction of quantified cuts
- On the generation of quantified lemmas
- A computational framework for conceptual blending
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- Proof mining with dependent types
- HipSpec
- Leon
- HR
- Hipster
- Cyclist
- QuickSpec
- InKa
- TIP
- Angelic Verification
- MATHsAiD
- QuodLibet
- TRANSIT
- Recycling proof patterns in Coq: case studies
- Dynamic rippling, middle-out reasoning and lemma discovery
- Theory exploration powered by deductive synthesis
- Hipster: integrating theory exploration in a proof assistant
- Automating Event-B invariant proofs by rippling and proof patching
- 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: IsaCoSy
