• 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 semi-automated reasoning systems have an adequate primary notion of proof ... systems and an appropriate level of abstraction for user-level 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, general-purpose operating-system 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 on-demand ... 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 real-time 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 well-typed ML program does...
  • PVS

  • Referenced in 634 articles [sw03484]
  • verification system: that is, a specification language integrated with support tools and a theorem prover ... state-of-the-art 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...
  • Bio-PEPA

  • Referenced in 108 articles [sw01361]
  • originally defined 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 object-oriented software as seamlessly as possible. At the core ... system is a novel theorem prover for the first-order 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 second-order 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 ”logics-as-theories” approach makes system behaviors as well as their represented knowledge ... provides an interface layer between formally rigorous mathematical systems, and knowledge management services which...