• MML

  • Referenced in 48 articles [sw06970]
  • large corpus of formalised mathematical knowledge. It has been constructed over the course of many ... communities of other libraries of formalised mathematical knowledge might take up the legal and scientific...
  • CAVA

  • Referenced in 2 articles [sw28570]
  • prover Isabelle. The algorithms are formalised on an mathematical, abstract level, using mainly sets...
  • Isabelle/UTP

  • Referenced in 13 articles [sw21184]
  • framework for the study, formalisation, and unification of formal semantics. Our contributions are, firstly ... tactics that transfer results from well-supported mathematical structures in Isabelle to proofs about...
  • NUML

  • Referenced in 1 article [sw03463]
  • NUML, there is the problem to formalise object- oriented programming paradigm which is still open ... with sufficient capability, which provides us a mathematical tool to do the formalization. This paper ... higher-order π-calculus to formalise NUML...
  • ForMaRE

  • Referenced in 3 articles [sw08774]
  • economics. The ForMaRE project applies formal mathematical reasoning to economics. We seek to increase confidence ... where we are building a toolbox of formalisations, and have started to study matching...
  • ASTRA

  • Referenced in 12 articles [sw00052]
  • Fault Tree Analysis (FTA) is a formalised deductive...
  • ACL2

  • Referenced in 283 articles [sw00060]
  • ACL2 is both a programming language in which...
  • Coq

  • Referenced in 1880 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Dafny

  • Referenced in 72 articles [sw00183]
  • Dafny is an imperative object-based language with...
  • GCLC

  • Referenced in 31 articles [sw00326]
  • We present GCLC/WinGCLC -- a tool for visualizing geometrical...
  • Isabelle

  • Referenced in 698 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • LEO-II

  • Referenced in 51 articles [sw00512]
  • LEO-II is a standalone, resolution-based higher...
  • Nitpick

  • Referenced in 63 articles [sw00622]
  • Nitpick is a counterexample generator for Isabelle/HOL that...
  • RelView

  • Referenced in 102 articles [sw00798]
  • The RelView-System is an interactive tool for...
  • Theorema

  • Referenced in 149 articles [sw00961]
  • The software system Theorema provides a uniform logic...
  • ML

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

  • Referenced in 723 articles [sw03455]
  • Spin is a popular open-source software tool...
  • Why3

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

  • Referenced in 654 articles [sw04702]
  • Uppaal is an integrated tool environment for modeling...