
Coq
 Referenced in 1906 articles
[sw00161]
 formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms...

SPIN
 Referenced in 727 articles
[sw03455]
 used for the formal verification of distributed software systems. The tool was developed at Bell...

UNITY
 Referenced in 185 articles
[sw13461]
 formal assertions, permitting formal verification of the transition systems, and second into an executable program ... correctness of the transition systems: one can specify properties formally that the model should obey...

Nuprl
 Referenced in 396 articles
[sw06751]
 Nuprl system is a framework for reasoning about mathematics and programming. Over the years ... base and supports the cooperation of independent formal tools...

Isar
 Referenced in 145 articles
[sw04599]
 reasoning systems include Coq, PVS, HOL, and Isabelle. Despite this success in actually formalizing parts ... none of the existing semiautomated reasoning systems have an adequate primary notion of proof ... systems and an appropriate level of abstraction for userlevel work. The Isar formal proof ... scripts. The Isabelle/Isar system provides an interpreter for the Isar formal proof document language. Isabelle/Isar...

ETPS
 Referenced in 161 articles
[sw06302]
 been used extensively under Unix and Linux systems, and to some extent under Windows. Potential ... development of formal theories in a wide variety of disciplines, deductive information systems for these ... report ETPS: A System to Help Students Write Formal Proofs (postscript...

seL4
 Referenced in 91 articles
[sw15222]
 Complete formal verification is the only known way to guarantee that a system is free ... unique design approach that fuses formal and operating systems techniques. To our knowledge, this ... first formal proof of functional correctness of a complete, generalpurpose operatingsystem kernel. Functional...

E Theorem Prover
 Referenced in 206 articles
[sw10187]
 order form. The system will then try to find a formal proof for the conjecture...

Flyspeck
 Referenced in 124 articles
[sw10277]
 that include islands of formal text. The formal text contains hyperlinks and gives ondemand ... that such a system significantly lowers the threshold for understanding formal development and facilitates collaboration ... formal development. To make this possible, we use the Agora system, a MathWiki platform developed...

Kronos
 Referenced in 274 articles
[sw01270]
 systems need to be rigorously modeled and specified in order to be able to formally ... requirements. In KRONOS, components of realtime systems are modeled by timed automata...

ML
 Referenced in 524 articles
[sw01218]
 polymorphic Hindley–Milner type system, which automatically assigns the types of most expressions without requiring ... ensures type safety – there is a formal proof that a welltyped ML program does...

PVS
 Referenced in 634 articles
[sw03484]
 verification system: that is, a specification language integrated with support tools and a theorem prover ... stateoftheart in mechanized formal methods and to be sufficiently rugged that...

LOTOS
 Referenced in 152 articles
[sw02961]
 specifically developed for the formal description of the OSI (Open Systems Interconnection) architecture, although...

BioPEPA
 Referenced in 108 articles
[sw01361]
 originally deﬁned for the performanceanalysis of computer systems, in order to handle some features ... seen as an intermediate, formal, compositional representation of biological systems, on which different kindsof analysis...

KeY
 Referenced in 65 articles
[sw09969]
 System is a formal software development tool that aims to integrate design, implementation, formal specification ... formal verification of objectoriented software as seamlessly as possible. At the core ... system is a novel theorem prover for the firstorder Dynamic Logic for Java with...

NetKAT
 Referenced in 23 articles
[sw16269]
 NetKAT  a formal system for the verification of networks. This paper presents a survey ... development of NetKAT, a formal system for reasoning about packet switching networks, and its role...

MPTP 0.2
 Referenced in 53 articles
[sw02589]
 Mizar Problems for Theorem Proving (MPTP) system and first experimental results obtained with ... MPTP project is to make the large formal Mizar Mathematical Library (MML) available to current ... formalism. The proofs using secondorder Mizar schemes are now handled by the system ... simple inductive or deductive system trained on formal mathematics can be sometimes smarter than...

K Prover
 Referenced in 45 articles
[sw32257]
 languages, calculi, as well as type systems or formal analysis tools can be defined, making...

MMT
 Referenced in 52 articles
[sw07136]
 level. This ”logicsastheories” approach makes system behaviors as well as their represented knowledge ... provides an interface layer between formally rigorous mathematical systems, and knowledge management services which...