Formal Methods Wiki
in: Content, Formal methods, Virtual Library

Formal methods

View source
VL2

Virtual Library
Computing
Software engineering
Formal methods

Wikipedia-word1 7

Formal methods


Formal methods are mathematical techniques for developing computer-based software and hardware systems.

Please update this page or add a new page if you know of relevant online information not included here or would like to maintain information on a particular topic. Use the comp.specification.misc newsgroup, for general formal methods queries. Please link to http://formalmethods.wikia.com if you create a permanent hyperlink to this website. In case of problems, please contact Jonathan Bowen.

Introduction

This document contains some pointers to information on Formal Methods↑, useful for mathematically describing and reasoning about computer-based systems, available around the world on the World Wide Web (WWW). Formal methods are a fault avoidance technique that help in the reduction of errors introduced into a system, particularly at the earlier stages of design. They complement fault removal techniques like testing. Links for accessing online information in the following categories are available:

! indicates new entries.
* indicates a (subjectively!) recommended link for especially good online information.

Selected resources

* This space will be used to indicate selected new entries and developments in these formal methods pages.

Individual notations, methods and tools

  1. * Abstract State Machines (ASM). Formerly known as Evolving Algebras.
  2. ACL2 (A Computational Logic for Applicative Common Lisp) theorem prover, a successor to the Nqthm Boyer-Moore theorem prover.
  3. ACSR (Algebra of Communicating Shared Resources) and Graphical Communicating Shared Resources (GCSR), a formal language for the specification, refinement, and analysis of real-time systems. See the tools VERSA (Verification Execution and Rewrite System for ACSR) and PARAGON for visual specification and verification of real-time systems.
  4. Action Semantics, a framework for specifying formal semantics of programming languages.
  5. Action systems for reasoning about distributed systems.
  6. aiT WCET Analyzer, an abstract interpretation based static analyzer that computes safe upper bounds for the worst-case execution time of tasks.
  7. * Alloy Analyzer, an object modelling notation that is compatible with development approaches such as UML, Catalysis, Fusion, OMT and Syntropy, strongly influenced by the Z specification language. See Alloy discussion group.
  8. Algebraic Design Language, a higher-order software specification language.
  9. Argos, an imperative synchronous language with verification support.
  10. Assertion Definition Language (ADL), a specification based testing toolset.
  11. Astrée, an abstract interpretation based static analyzer that proves the absence of runtime errors in C programs.
  12. Autofocus for specifying distributed systems. First prize winner in the tool competition at FM'99.
  13. BDDs (Binary Decision Diagrams) for finite-state verification problems.
  14. * B-Method, including the B-Tool and B-Toolkit.
  15. Boyer-Moore theorem prover (a forerunner of Nqthm and ACL2). Available via ICOT Free Software for use under Unix at ICOT (Japan).
  16. * CADP: a widespread toolbox for the Construction and Analysis of Distributed Processes, developed at INRIA Grenoble
  17. * CASL: Common Algebraic Specification Language, for algebraic specification and development, from CoFI, the Common Framework Initiative.
  18. * CafeOBJ, an algebraic specification and programming language. A successor of OBJ.
  19. * CCS (Calculus of Communicating Systems). A process algebra for concurrent systems.
  20. Circal (CIRcuit CALculus) System supporting a process algebra which may be used to rigorously describe, verify and simulate concurrent systems. See software.
  21. CLaReT: The Computer Language Reasoning Tool.
  22. COLD (Common Object-oriented Language for Design), a wide-spectrum specification language.
  23. CommUnity, based on category theory. See also CommUnity Workbench.
  24. Concurrency Factory, a "next generation" Concurrency Workbench toolkit.
  25. * Coq proof assistant: checks proofs about assertions, helps to find formal proofs and extracts certified programs from constructive proofs.
  26. * CSP (Communicating Sequential Processes) including the FDR2 (Failures-Divergence Refinement) tool.
  27. CWB Concurrency Factory and CWB-NC (The Concurrency Workbench of North Carolina), which includes a LOTOS interface, diagnostic information, etc. Note: The CWB and CWB-NC have a common ancestor, but are each under separate development.
  28. dL -- differential dynamic logic for hybrid systems verification.
  29. DisCo specification method for reactive systems including an animation tool, Finland.
  30. *Duration Calculus (DC), an interval logic for real-time systems.
  31. *ESC/Java2 Extended Static Checker for Java tool, using program verification technology. See also JML.
  32. * Escher C Verifier, a tool for formal verification of embedded software written in MISRA-C.
  33. Estelle Formal Description Technique (IS 9074). See also EDT (Estelle Development Toolset).
  34. * Esterel language and tools for synchronous reactive systems.
  35. EVES tool, based on ZF set theory, from ORA, Canada. See also Z/EVES which provides a Z notation front-end to EVES.
  36. Extended ML framework for the specification and formal development of modular Standard ML programs.
  37. FermaT program transformation system. See also here.
  38. FormalCheck model checker tool for verifying the functionality of digital hardware designs in Verilog or VHDL, based on the COSPAN model checker.
  39. * HOL mechanical theorem proving system, based on Higher Order Logic.
  40. HyTech (The HYbrid TECHnology Tool), an automatic tool for the analysis of embedded systems which computes the condition under which a linear hybrid system satisfies a temporal-logic requirement.
  41. * IMPS, an Interactive Mathematical Proof System intended to provide mechanical support for traditional mathematical techniques and styles of practice.
  42. * Interval Temporal Logic (ITL). See also and Temporal and Logic publications.
  43. * Isabelle, a generic theorem prover, supporting higher-order logic, ZF set theory, etc.
  44. Jape (Just Another Proof Editor). A framework for building interactive proof editors.
  45. * JML (Java Modeling Language), a behavioral interface specification language for Java. See also ESC/Java2.
  46. KeY An automatic and interactive, verification and test generation tool for Java Card.
  47. KeYmaera A Hybrid Theorem Prover for Hybrid Systems.
  48. KIV (Karlsruhe Interactive Verifier). A tool for the development of correct software using stepwise refinement.
  49. Kronos, a verification tool for safety and liveness properties of real-time systems. Uses timed automata, TCTL (an extension of temporal logic) and model-checking.
  50. * Larch family of languages and tools supporting a two-tiered definitional style of specification. See especially LP, the Larch Prover.
  51. LeanTAP, a tableau-based deduction theorem prover for classical first-order logic.
  52. LEGO proof assistant.
  53. Leo-II resolution-based automated theorem prover for Higher-Order Logic
  54. * LOTOS (Language of Temporal Ordering Specifications).
  55. LPV Linear Programming based software Validation technology, including proofs and testing.
  56. Lustre synchronous declarative language for programming reactive systems, including verification.
  57. MALPAS static analysis tool-set.
  58. Maintainer's Assistant, a tool for reverse engineering and re-engineering code using formal methods.
  59. MathSpad structure editor, especially for mathematical calculations.
  60. Maude system for equational and rewriting logic specification and programming. Influenced by OBJ3.
  61. Meije tools for the verification of concurrent programs. Includes ATG, a graphical editor/visualizer.
  62. μCRL (micro CRL), process algebraic language for communicating processes with data.
  63. mCRL2 a toolset for a process algebraic language and a modal logic with data and time. Successor of μCRL.
  64. Mizar System, a long-term effort aimed at developing software to support a working mathematician in preparing papers. See also here.
  65. * Model checking at CMU, a method for formally verifying finite-state concurrent systems. Available packages include:
    • BDD library with extensions for sequential verification.
    • CV, a VHDL model checker.
    • CSML and MCB, a language for compositional description of finite state machines and a (non-symbolic) model checker for CTL.
    • SMV (Symbolic Model Verifier) model checker for finite-state systems, using the specification language CTL (Computation Tree Logic), a propositional branching-time temporal logic. See also Word-level SMV for verifying arithmetic circuits efficiently. See also * NuSMV, a new symbolic model checker.
  66. Murphi description language and verifier tool for finite-state verification of concurrent systems.
  67. * Nqthm 1992, the latest Boyer-Moore theorem prover. Also accessible via FTP. Includes the Pc-Nqthm interactive Proof-checker.
  68. * Nuprl tool based on intuitionistic type theory.
  69. * OBJ family — OBJ3, 2OBJ, CafeOBJ, etc. Term rewriting and algebraic specification.
  70. OCL (Object Constraint Language), part of UML.
  71. Otter, an automated deduction system.
  72. PEPA, a stochastic process algebra used for modelling systems composed of concurrently active components that co-operate and share work.
  73. * Perfect Developer tool from Escher Techologies Limited.
  74. * Petri Nets, a formal graphical notation for modelling systems with concurrency. See also here.
  75. * Pi-calculus: calculi for mobile processes. See also the Mobility Workbench and a searchable bibliography.
  76. Pobl. A development method for concurrent object-based programs.
  77. ProofPower is a commercial tool, developed by ICL, supporting development and checking of specifications and formal proofs in Higher Order Logic and/or Z. Support for Z uses a deep(ish) embedding of Z into HOL, but includes syntax and type checking customized for Z.
  78. Prover Technology, commercial proof engines.
  79. * PVS (Prototype Verification System) language and tool based on classical typed higher-order logic.
  80. * RAISE (Rigorous Approach to Industrial Software Engineering). Includes RSL (RAISE Specification Language).
  81. Rapide language and toolset, for building large-scale distributed multi-language systems.
  82. Refinement Calculus, a formalisation of the stepwise refinement method of program construction.
  83. RISC ProgramExplorer, a computer-supported program reasoning environment for educational purposes.
  84. SCR (Software Cost Reduction), a tabular notation for specifying requirements and tools for creating and analyzing requirements specifications.
  85. * SDL (Specification and Description Language) from the SDL Forum Society. See also previous site here.
  86. Signal/Polychrony language and toolset for synchronous systems. See also the related Esterel and Lustre.
  87. * SPARK (now AltranPraxis) secure subset of Ada, including the SPADE static analysis toolset.
  88. * Spec#, an extension of the C# programming language from Microsoft Research with specification features allowing static analysis using a program verifier.
  89. Specware automated software development system for stepwise refinement of provably correct code. See also technology transfer information and publication from the Kestrel Institute.
  90. * SPIN is an automated verification tool (model checker), using PROMELA (PROcess MEta LAnguage), a language loosely based on CSP, for finite state systems, such as protocols or validation models of distributed systems, developed at Bell Laboratories. See also p2b, a translation utility.
  91. StackAnalyzer, an abstract interpretation based static analyzer for computing the worst-case stack usage of tasks.
  92. StateSim simulator for Statecharts models. Draw your models in Open Office Draw and the run your simulations from StateSim.
  93. Statestep finite state machine modelling with comprehensive elicitation of unusual scenarios (addressing "corner cases" or the feature interaction problem).
  94. STeP, the Stanford Temporal Prover.
  95. TAM'97 (Trace Assertion Method). A formal method for abstract specification of module interfaces.
  96. Temporal-Rover — formal specification and testing tool based on temporal logic.
  97. TLA (Temporal Logic of Actions), a logic for specifying and reasoning about concurrent and reactive systems.
  98. TPS and ETPS, the Theorem Proving System and the Educational Theorem Proving System.
  99. TRIO language and tools for real-time systems, based on temporal logic.
  100. TTM/RTTL framework for real-time reactive systems.
  101. UNITY, a programming notation and a logic to reason about parallel and distributed programs.
  102. UPPAAL verification and validation tools for real-time systems. Model checking and simulation with a graphical interface.
  103. VCC, Microsoft Research - Verification of Concurrent C; a sound deductive verifier for C.
  104. VeriSoft, Bell Laboratories, Lucent Technologies. A model checking tool for systematic software testing of concurrent/reactive/real-time systems. Automatically searches for coordination problems (deadlocks, etc.) and assertion violations. Supports C, C++, etc.
  105. * VDM (Vienna Development Method). See also Overture toolset.
  106. VIS (Verification Interacting with Synthesis), a system for formal verification, synthesis, and simulation of finite state systems, especially logic circuits. Includes a Verilog HDL front-end.
  107. X-machines, related to finite state machines.
  108. * Z notation for formal specification and extensions eg. TCOZ (Timed Communicating Object Z) .

See also:

Newsgroups and mailing lists

The following electronic mailing lists cover general issues concerning formal methods:

There are a significant number of mailing lists concerning individual formal methods. Please see the relevant pages for the formal methods of interest for details.

Of related interest

See also information on:

Cited in W.W. Gibbs, Software's Chronic Crisis, Scientific American, 271(3):86-95, September 1994.

See also FormalMethods.com. :-)

Last updated by Jonathan Bowen, 11 March 2021.
Further information for possible inclusion is welcome.

Community content is available under CC-BY-SA unless otherwise noted.