Results 1 to 20 of 254
Sort by:

  • 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 116 articles [sw07047]
  • discharge interactive proof obligations arising in Isabelle/HOL. We extended it with LEO-II and Satallax...

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

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

  • CeTA
  • Referenced in 42 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...