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

PVS
 Referenced in 624 articles
[sw03484]
 stateoftheart in mechanized formal methods and to be sufficiently rugged that...

HOL Light
 Referenced in 296 articles
[sw06580]
 some nontrivial 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 computerchecked 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 ... 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 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 ondemand 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 chisquared tests) and model...