• PIDE

  • Referenced in 11 articles [sw06404]
  • overall aim is to connect LCF-style provers like Isabelle...
  • IsaWin

  • Referenced in 8 articles [sw04899]
  • metaphor suited to visualize the LCF-style prover design, and a methodology for the implementation...
  • Psyche

  • Referenced in 5 articles [sw28518]
  • based on sequent calculus with an LCF-style architecture. Psyche is a modular proof-search...
  • Squolem

  • Referenced in 3 articles [sw09453]
  • results. Detailed performance data shows that LCF-style certificate checking is feasible even for large...
  • ACL2

  • Referenced in 291 articles [sw00060]
  • ACL2 is both a programming language in which...
  • Isabelle

  • Referenced in 719 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • MiniSat

  • Referenced in 584 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...
  • ML

  • Referenced in 524 articles [sw01218]
  • ML (’Meta Language’) is a general-purpose functional...
  • SATLIB

  • Referenced in 59 articles [sw02107]
  • SATLIB is a collection of benchmark problems, solvers...
  • KRAKATOA

  • Referenced in 89 articles [sw03159]
  • The KRAKATOA tool for certification of JAVA/JAVACARD programs...
  • PVS

  • Referenced in 634 articles [sw03484]
  • PVS is a verification system: that is, a...
  • Why3

  • Referenced in 136 articles [sw04438]
  • Why3 is a platform for deductive program verification...
  • Isar

  • Referenced in 145 articles [sw04599]
  • Theorem proving system supporting both interactive proof development...
  • zChaff

  • Referenced in 37 articles [sw04757]
  • zChaff is an implementation of the well known...
  • HOL

  • Referenced in 594 articles [sw05492]
  • Higher Order Logic (HOL) is a programming environment...