Quick specifications for the busy programmer
From MaRDI portal
Recommendations
- Automating Inductive Proofs Using Theory Exploration
- The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
- Testing and tracing lazy functional programs using QuickCheck and Hat
- Fully Automatic Testing with Functions as Specifications
- Smart testing of functional programs in Isabelle
Cites work
- scientific article; zbMATH DE number 44213 (Why is no real title available?)
- scientific article; zbMATH DE number 1439160 (Why is no real title available?)
- Automating Inductive Proofs Using Theory Exploration
- Conjecture synthesis for inductive theories
- Functional geometry
- Hipster: integrating theory exploration in a proof assistant
- Ordered rewriting and confluence
- The Daikon system for dynamic detection of likely invariants
- The octonions
- Zur Struktur von Alternativkörpern
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
Cited in
(6)- Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
- Into the Infinite - Theory Exploration for Coinduction
- Lemma discovery and strategies for automated induction
- Conjectures, tests and proofs: an overview of theory exploration
- Theory exploration powered by deductive synthesis
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
Describes a project that uses
Uses Software
This page was built for publication: Quick specifications for the busy programmer
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5371995)
