• Isar

  • Referenced in 138 articles [sw04599]
  • current end-user setup is mainly for Isabelle/HOL. Together with the Isabelle/Isar instantiation of Proof...
  • Sledgehammer

  • Referenced in 114 articles [sw07047]
  • discharge interactive proof obligations arising in Isabelle/HOL. We extended it with LEO-II and Satallax...
  • Nominal Isabelle

  • Referenced in 67 articles [sw12055]
  • Isabelle is a definitional extension of the Isabelle/HOL theorem prover. It provides a proving infrastructure...
  • Nitpick

  • Referenced in 54 articles [sw00622]
  • Nitpick is a counterexample generator for Isabelle/HOL that builds on Kodkod, a SAT-based first...
  • CeTA

  • Referenced in 41 articles [sw06584]
  • this paper we use the theorem prover Isabelle/HOL to automatically certify termination proofs. To this...
  • Ott

  • Referenced in 30 articles [sw00663]
  • proof assistant code for Coq, HOL, and Isabelle/HOL, together with LaTeX code for production-quality...
  • Transfer

  • Referenced in 26 articles [sw21009]
  • Transfer: A Modular Design for Quotients in Isabelle/HOL. Quotients, subtypes, and other forms of type...
  • Lifting

  • Referenced in 26 articles [sw21010]
  • Transfer: A Modular Design for Quotients in Isabelle/HOL. Quotients, subtypes, and other forms of type...
  • CCSL

  • Referenced in 25 articles [sw03357]
  • logic either for PVS or for for Isabelle/HOL (in new style Isar syntax). After translation...
  • MaSh

  • Referenced in 21 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...
  • Autoref

  • Referenced in 14 articles [sw12809]
  • refinement. We present the Autoref tool for Isabelle/HOL, which automatically refines algorithms specified over abstract...
  • Isabelle/Circus

  • Referenced in 13 articles [sw15208]
  • semantic theory of UTP based on Isabelle/HOL). We derive proof rules from this semantics...
  • Berlekamp Zassenhaus

  • Referenced in 8 articles [sw28596]
  • factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization ... dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using Isabelle...
  • HOL-Z

  • Referenced in 11 articles [sw02996]
  • plug-in of the generic theorem prover Isabelle/HOL (Version 2005). It allows for importing...
  • Isabelle/UTP

  • Referenced in 10 articles [sw21184]
  • unifying theories of programming (UTP) in Isabelle/HOL. UTP is a framework for the study, formalisation...
  • RALL

  • Referenced in 9 articles [sw08505]
  • system is an advanced case study for Isabelle/HOL, and on the other hand, a quite...
  • Presburger Automata

  • Referenced in 9 articles [sw28603]
  • strings in the theorem prover Isabelle/HOL. It forms the basis of a reflection-based decision...