
Coq
 Referenced in 1784 articles
[sw00161]
 formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms ... machinechecked 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 welltyped 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]
 stateoftheart in mechanized formal methods and to be sufficiently rugged that...

HOL Light
 Referenced in 288 articles
[sw06580]
 some nontrivial 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 computerchecked 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 ... semiautomated reasoning (Isar) approach to readable formal proof documents sets out to bridge ... abstraction for userlevel 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 ondemand 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 chisquared tests) and model...