• Coq

  • Referenced in 1784 articles [sw00161]
  • formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms ... machine-checked proofs. Typical applications include the formalization of programming languages semantics (e.g. the CompCert ... Card EAL7 certification in industrial context), the formalization of mathematics (e.g. the full formalization...
  • Isabelle/HOL

  • Referenced in 945 articles [sw01569]
  • mathematical formulas to be expressed in a formal language and provides tools for proving those ... logical calculus. The main application is the formalization of mathematical proofs and in particular formal...
  • Isabelle

  • Referenced in 606 articles [sw00454]
  • mathematical formulas to be expressed in a formal language and provides tools for proving those ... logical calculus. The main application is the formalization of mathematical proofs and in particular formal...
  • ML

  • Referenced in 514 articles [sw01218]
  • ensures type safety – there is a formal proof that a well-typed ML program does ... completely specified and verified using formal semantics. Its types and pattern matching make it well ... commonly used to operate on other formal languages, such as in compiler writing, automated theorem ... proving and formal verification. (wikipedia...
  • SPIN

  • Referenced in 709 articles [sw03455]
  • worldwide, that can be used for the formal verification of distributed software systems. The tool...
  • PVS

  • Referenced in 614 articles [sw03484]
  • state-of-the-art in mechanized formal methods and to be sufficiently rugged that...
  • HOL Light

  • Referenced in 288 articles [sw06580]
  • some non-trivial tasks in the formalization of mathematics and industrial formal verification...
  • Nuprl

  • Referenced in 387 articles [sw06751]
  • base and supports the cooperation of independent formal tools...
  • UNITY

  • Referenced in 184 articles [sw13461]
  • transition systems first into a set of formal assertions, permitting formal verification of the transition ... transition systems: one can specify properties formally that the model should obey and prove them ... theorems using the formal specification. The methodology is illustrated through generation of a simulation program...
  • OTTER

  • Referenced in 313 articles [sw02904]
  • Otter is research in abstract algebra and formal logic. Otter and its predecessors have been...
  • NuSMV

  • Referenced in 295 articles [sw04131]
  • custom verification tools, as a testbed for formal verification techniques, and applied to other research...
  • Z

  • Referenced in 278 articles [sw10291]
  • this adquate for promoting a discipline of formal specification and reasoning? Another disappointment is that...
  • Archive Formal Proofs

  • Referenced in 152 articles [sw28613]
  • Isabelle’s Archive of Formal Proofs (AFP): Mining the Archive of Formal Proofs. The Archive ... Formal Proofs is a vast collection of computer-checked proofs developed using the proof assistant ... gives some insights into the nature of formal proofs...
  • Kronos

  • Referenced in 261 articles [sw01270]
  • specified in order to be able to formally prove their correctness with respect...
  • AUSM

  • Referenced in 256 articles [sw06367]
  • limit. Specifically, we employ asymptotic analysis to formally derive proper scalings for the numerical fluxes...
  • Isar

  • Referenced in 140 articles [sw04599]
  • Isabelle. Despite this success in actually formalizing parts of mathematics and computer science, there ... semi-automated reasoning (Isar) approach to readable formal proof documents sets out to bridge ... abstraction for user-level work. The Isar formal proof language has been designed to satisfy ... system provides an interpreter for the Isar formal proof document language. Isabelle/Isar input consists either...
  • Flyspeck

  • Referenced in 111 articles [sw10277]
  • Communicating formal proofs: the case of flyspeck. We introduce a platform for presenting and cross ... linking formal and informal proof developments together. The platform supports writing natural language `narratives’ that ... include islands of formal text. The formal text contains hyperlinks and gives on-demand state ... system significantly lowers the threshold for understanding formal development and facilitates collaboration on informal...
  • ETPS

  • Referenced in 153 articles [sw06302]
  • various mathematical activities, promoting development of formal theories in a wide variety of disciplines, deductive ... ETPS: A System to Help Students Write Formal Proofs (postscript...
  • E Theorem Prover

  • Referenced in 191 articles [sw10187]
  • system will then try to find a formal proof for the conjecture, assuming the axioms...
  • spatstat

  • Referenced in 129 articles [sw04429]
  • fitting, simulation, spatial sampling, model diagnostics, and formal inference. Data types include point patterns, line ... simulated automatically. Also provides facilities for formal inference (such as chi-squared tests) and model...