• 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...
  • 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...