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

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

HOL Light
 Referenced in 308 articles
[sw06580]
 some nontrivial tasks in the formalization of mathematics and industrial formal verification...

Nuprl
 Referenced in 394 articles
[sw06751]
 base and supports the cooperation of independent formal tools...

Archive Formal Proofs
 Referenced in 178 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...

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 309 articles
[sw04131]
 custom verification tools, as a testbed for formal verification techniques, and applied to other research...

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

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

Kronos
 Referenced in 273 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 121 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 160 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 199 articles
[sw10187]
 system will then try to find a formal proof for the conjecture, assuming the axioms...

spatstat
 Referenced in 140 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...