Results 1 to 20 of 203
Sort by:

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