• Coq

  • Referenced in 1360 articles [sw00161]
  • proof management system. It provides a formal language to write mathematical definitions, executable algorithms ... proofs. Typical applications include the formalization of programming languages semantics (e.g. the CompCert compiler certification ... Card EAL7 certification in industrial context), the formalization of mathematics (e.g. the full formalization...
  • Isabelle/HOL

  • Referenced in 702 articles [sw01569]
  • formulas to be expressed in a formal language and provides tools for proving those formulas ... logical calculus. The main application is the formalization of mathematical proofs and in particular formal ... software and proving properties of computer languages and protocols...
  • ML

  • Referenced in 449 articles [sw01218]
  • Language’) is a general-purpose functional programming language. It has roots in Lisp ... ensures type safety – there is a formal proof that a well-typed ML program does ... languages to be completely specified and verified using formal semantics. Its types and pattern matching ... commonly used to operate on other formal languages, such as in compiler writing, automated theorem...
  • Isabelle

  • Referenced in 458 articles [sw00454]
  • formulas to be expressed in a formal language and provides tools for proving those formulas ... logical calculus. The main application is the formalization of mathematical proofs and in particular formal ... software and proving properties of computer languages and protocols...
  • Isar

  • Referenced in 115 articles [sw04599]
  • user-level work. The Isar formal proof language has been designed to satisfy quite contradictory ... system offers Isar as an alternative proof language interface layer, beyond traditional tactic scripts ... interpreter for the Isar formal proof document language. Isabelle/Isar input consists either of proper document...
  • AVISPA

  • Referenced in 70 articles [sw03172]
  • provides a modular and expressive formal language for specifying protocols and their security properties...
  • Isabelle/ZF

  • Referenced in 52 articles [sw04973]
  • formulas to be expressed in a formal language and provides tools for proving those formulas ... logical calculus. The main application is the formalization of mathematical proofs and in particular formal ... proving properties of computer languages and protocols. Isabelle/ZF formalizes the greater part of elementary...
  • Matita

  • Referenced in 53 articles [sw06140]
  • machine collaboration. It provides a formal language where mathematical definitions, executable algorithms and theorems cohexist...
  • PDDL

  • Referenced in 80 articles [sw07079]
  • describe the syntax of the language, its formal semantics and the validation of concurrent plans...
  • PVS

  • Referenced in 530 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...
  • LEGO

  • Referenced in 62 articles [sw09685]
  • more practical by bringing the level of formalization closer to that of informal mathematics ... inductive types, provide an expressive language for formalization of mathematical problems and program specification...
  • GF

  • Referenced in 30 articles [sw13667]
  • theoretical grammar formalism. Grammatical Framework (GF) is a special-purpose functional language for defining grammars ... strings. GF can describe both formal and natural languages. The key notion of this description ... natural languages, or precedence in formal languages. Grammatical objects have a type system, which helps ... trees can simultaneously be viewed in different languages. This paper starts with a gradual introduction...
  • Bandera

  • Referenced in 129 articles [sw07663]
  • software requirement formalized in Bandera’s temporal specification language, and it generates a program model...
  • Flyspeck

  • Referenced in 84 articles [sw10277]
  • platform supports writing natural language `narratives’ that include islands of formal text. The formal text...
  • BLOG

  • Referenced in 31 articles [sw22025]
  • paper introduces and illustrates BLOG, a formal language for defining probability models over worlds with...
  • LOTOS

  • Referenced in 144 articles [sw02961]
  • specification language that has been specifically developed for the formal description of the OSI (Open...
  • GHC

  • Referenced in 42 articles [sw23765]
  • close relationship to other formalisms including dataflow languages, Communicating Sequential Processes, and functional languages...
  • E-LOTOS

  • Referenced in 23 articles [sw03017]
  • formality to UML. E-LOTOS, a new version of the ISO standard specification language LOTOS ... used to give a formal meaning to, and to discover inconsistencies in, UML models ... this can be modelled in a formal language...
  • JUnit

  • Referenced in 23 articles [sw07262]
  • unit tests easier. It uses a formal specification language’s runtime assertion checker to decide ... writing testing code, the programmer writes formal specifications (e.g., pre- and postconditions). This makes ... implemented this idea using the Java Modeling Language (JML) and the JUnit testing framework ... easily implemented with other combinations of formal specification languages and unit test tools...
  • ConGolog

  • Referenced in 46 articles [sw01801]
  • ConGolog, a concurrent programming language based on the situation calculus As an alternative to planning ... considered. A formal definition in the situation calculus of such a programming language is presented ... with exogenous actions. The language differs from other procedural formalisms for concurrency in that ... situation calculus. Some mathematical properties of the language are proven, for instance, that the proposed...