-
Isar
- Referenced in 125 articles
[sw04599]
- current end-user setup is mainly for Isabelle/HOL. Together with the Isabelle/Isar instantiation of Proof...
-
Sledgehammer
- Referenced in 101 articles
[sw07047]
- discharge interactive proof obligations arising in Isabelle/HOL. We extended it with LEO-II and Satallax...
-
Nominal Isabelle
- Referenced in 62 articles
[sw12055]
- Isabelle is a definitional extension of the Isabelle/HOL theorem prover. It provides a proving infrastructure...
-
Nitpick
- Referenced in 46 articles
[sw00622]
- Nitpick is a counterexample generator for Isabelle/HOL that builds on Kodkod, a SAT-based first...
-
CeTA
- Referenced in 39 articles
[sw06584]
- this paper we use the theorem prover Isabelle/HOL to automatically certify termination proofs. To this...
-
Ott
- Referenced in 25 articles
[sw00663]
- proof assistant code for Coq, HOL, and Isabelle/HOL, together with LaTeX code for production-quality...
-
CCSL
- Referenced in 25 articles
[sw03357]
- logic either for PVS or for for Isabelle/HOL (in new style Isar syntax). After translation...
-
Transfer
- Referenced in 19 articles
[sw21009]
- Transfer: A Modular Design for Quotients in Isabelle/HOL. Quotients, subtypes, and other forms of type...
-
Lifting
- Referenced in 19 articles
[sw21010]
- Transfer: A Modular Design for Quotients in Isabelle/HOL. Quotients, subtypes, and other forms of type...
-
MaSh
- Referenced in 17 articles
[sw08206]
- automatic theorem provers in the proof assistant Isabelle/HOL. A key component, the relevance filter, heuristically...
-
HOL-Boogie
- Referenced in 14 articles
[sw00409]
- combines Boogie with the interactive theorem prover Isabelle/HOL. In particular, we present specific techniques combining...
-
Isabelle/Circus
- Referenced in 13 articles
[sw15208]
- semantic theory of UTP based on Isabelle/HOL). We derive proof rules from this semantics...
-
HOL-Z
- Referenced in 11 articles
[sw02996]
- plug-in of the generic theorem prover Isabelle/HOL (Version 2005). It allows for importing...
-
Autoref
- Referenced in 10 articles
[sw12809]
- refinement. We present the Autoref tool for Isabelle/HOL, which automatically refines algorithms specified over abstract...
-
RALL
- Referenced in 9 articles
[sw08505]
- system is an advanced case study for Isabelle/HOL, and on the other hand, a quite...
-
HOL-TestGen
- Referenced in 9 articles
[sw17720]
- specfication and theorem proving environment Isabelle/HOL...
-
Isabelle/UTP
- Referenced in 9 articles
[sw21184]
- unifying theories of programming (UTP) in Isabelle/HOL. UTP is a framework for the study, formalisation...
-
Refinement Monadic
- Referenced in 6 articles
[sw28551]
- framework for program and data refinement in Isabelle/HOL. The framework is based on a nondeterminism ... form that is accepted by the Isabelle/HOL code generator...
-
IsaFoR
- Referenced in 5 articles
[sw10106]
- functions in (a first-order subset of) Isabelle/HOL by encoding them as term rewrite systems ... where all necessary properties are derived inside Isabelle/HOL without oracles. Apart from the certification ... reduction of the proof obligation produced by Isabelle/HOL to the termination of the corresponding term...