• Coq

  • Referenced in 1828 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 978 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 622 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 517 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 715 articles [sw03455]
  • worldwide, that can be used for the formal verification of distributed software systems. The tool...
  • PVS

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

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

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

  • Referenced in 185 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 316 articles [sw02904]
  • Otter is research in abstract algebra and formal logic. Otter and its predecessors have been...
  • NuSMV

  • Referenced in 299 articles [sw04131]
  • custom verification tools, as a testbed for formal verification techniques, and applied to other research...
  • Archive Formal Proofs

  • Referenced in 163 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...
  • Z

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

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

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

  • Referenced in 144 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 114 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 157 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 196 articles [sw10187]
  • system will then try to find a formal proof for the conjecture, assuming the axioms...
  • spatstat

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