Text-only access using Betsie [Formal Methods Europe (FME)] [Centre for Applied Formal Methods (CAFM), London South Bank University, UK] * Virtual Library   * Computing   * Software Engineering   * Education

Formal Methods

Please contact Jonathan Bowen if you know of relevant on-line 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://vl.fmnet.info/ if you create a permanent hyperlink to this website.

__________

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 on-line information in the following categories are available:

! indicates new entries. * indicates a (subjectively!) recommended link for especially good on-line information. If enough people email me, I will add a star to entries recommended by others.

* Selected resources: This space will be used to indicate selected new entries and developments in the 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. * 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.

  7. Autofocus for specifying distributed systems. First prize winner in the tool competition at FM'99.

  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. BDDs (Binary Decision Diagrams) for finite-state verification problems.

  12. * B-Method, including the B-Tool and B-Toolkit.

  13. Boyer-Moore theorem prover (a forerunner of Nqthm and ACL2). Available via ICOT Free Software for use under Unix at ICOT (Japan).

  14. * CASL: Common Algebraic Specification Language, for algebraic specification and development, from CoFI, the Common Framework Initiative.

  15. * CafeOBJ, an algebraic specification and programming language. A successor of OBJ.

  16. CCS (Calculus of Communicating Systems). An algebra for specifying and reasoning about concurrent systems. See tool support and Communication and Concurrency book.

  17. Circal (CIRcuit CALculus) System supporting a process algebra which may be used to rigorously describe, verify and simulate concurrent systems. See software.

  18. CLaReT: The Computer Language Reasoning Tool.

  19. COLD (Common Object-oriented Language for Design), a wide-spectrum specification language.

  20. CommUnity, based on category theory. See also CommUnity Workbench.

  21. Concurrency Factory, a "next generation" Concurrency Workbench toolkit.

  22. * Coq proof assistant: checks proofs about assertions, helps to find formal proofs and extracts certified programs from constructive proofs.

  23. * CSP (Communicating Sequential Processes) including the FDR2 (Failures-Divergence Refinement) tool.

  24. CWB Concurrency Factory and CWB-NC (The Concurrency Workbench of North Carolina), which includes a LOTOS interface, diagnostic infomation, etc. Note: The CWB and CWB-NC have a common ancestor, but are each under separate development.

  25. DisCo specification method for reactive systems including an animation tool, Finland.

  26. * Duration Calculus (DC), an interval logic for real-time systems.

  27. * ESC/Java2 Extended Static Checker for Java tool, using program verification technology. See also JML.

  28. Estelle Formal Description Technique (IS 9074). See also EDT (Estelle Development Toolset).
  29. * Esterel language and tools for synchronous reactive systems.

  30. EVES tool, based on ZF set theory, from ORA, Canada. See also Z/EVES which provides a Z notation front-end to EVES.

  31. Extended ML framework for the specification and formal development of modular Standard ML programs.

  32. FermaT program transformation system. See also here.

  33. FormalCheck model checker tool for verifying the functionality of digital hardware designs in Verilog or VHDL, based on the COSPAN model checker.

  34. * HOL mechanical theorem proving system, based on Higher Order Logic.

  35. 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.

  36. * IMPS, an Interactive Mathematical Proof System intended to provide mechanical support for traditional mathematical techniques and styles of practice.

  37. * Interval Temporal Logic (ITL). See also publications.

  38. * Isabelle, a generic theorem prover, supporting higher-order logic, ZF set theory, etc.

  39. Jape (Just Another Proof Editor). A framework for building interactive proof editors.

  40. * JML (Java Modeling Language), a behavioral interface specification language for Java. See also ESC/Java2.

  41. ! KIV (Karlsruhe Interactive Verifier). An interactive theorem prover for higher-order logic, Dynamic Logic and a compositional extension of ITL. It can be used for ASM stepwise refinement.

  42. 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.

  43. * Larch family of languages and tools supporting a two-tiered definitional style of specification. See especially LP, the Larch Prover.

  44. LeanTAP, a tableau-based deduction theorem prover for classical first-order logic.

  45. LEGO proof assistant.

  46. * LOTOS (Language of Temporal Ordering Specifications).

  47. LPV Linear Programming based software Validation technology, including proofs and testing.

  48. Lustre synchronous declarative language for programming reactive systems, including verification.

  49. MALPAS static analysis tool-set.

  50. Maintainer's Assistant, a tool for reverse engineering and re-engineering code using formal methods.

  51. MathSpad structure editor, especially for mathematical calculations.

  52. Maude system for equational and rewriting logic specification and programming. Influenced by OBJ3.

  53. Meije tools for the verification of concurrent programs. Includes ATG, a graphical editor/visualizer.

  54. µCRL (micro CRL), process algebraic language for communicating processes with data.

  55. Mizar System, a long-term effort aimed at developing software to support a working mathematician in preparing papers. See also here.

  56. * 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.

  57. Murphi description language and verifier tool for finite-state verification of concurrent systems.

  58. * Nqthm 1992, the latest Boyer-Moore theorem prover. Also accessible via FTP. Includes the Pc-Nqthm interactive ``Proof-checker''.

  59. * Nuprl tool based on intuitionistic type theory.

  60. * OBJ family - OBJ3, 2OBJ, CafeOBJ, etc. Term rewriting and algebraic specification.

  61. OCL (Object Constraint Language), part of UML.

  62. Otter, an automated deduction system.

  63. PEPA, a stochastic process algebra used for modelling systems composed of concurrently active components that co-operate and share work.

  64. * Perfect Developer tool from Escher Techologies Limited.

  65. * Petri Nets, a formal graphical notation for modelling systems with concurrency. See also here.

  66. * Pi-calculus: calculi for mobile processes. See also the Mobility Workbench and a searchable bibliography.

  67. Pobl. A development method for concurrent object-based programs.

  68. 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.

  69. Prover Technology, commercial proof engines.

  70. * PVS (Prototype Verification System) tool based on classical typed higher-order logic.

  71. * RAISE (Rigorous Approach to Industrial Software Engineering). Includes RSL (RAISE Specification Language).

  72. Rapide language and toolset, for building large-scale distributed multi-language systems.

  73. Refinement Calculus, a formalisation of the stepwise refinement method of program construction.

  74. SCR (Software Cost Reduction), a tabular notation for specifying requirements and tools for creating and analyzing requirements specifications.

  75. * SDL (Specification and Description Language) from the SDL Forum Society. See also previous site here.

  76. Signal/Polychrony language and toolset for synchronous systems. See also the related Esterel amd Lustre.

  77. * SPARK secure subset of Ada, including the SPADE static analysis toolset.

  78. * Spec#, an extension of the C# programming language from Microsoft Research with specification features allowing static analysis using a program verifier.

  79. Specware automated software development system for stepwise refinement of provably correct code. See also technology transfer information and publication from the Kestrel Institute.

  80. * 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.

  81. Statestep interactive specification tool.

  82. STeP, the Stanford Temporal Prover.

  83. TAM'97 (Trace Assertion Method). A formal method for abstract specification of module interfaces.

  84. Temporal-Rover - formal specification and testing tool based on temporal logic.

  85. TLA (Temporal Logic of Actions), a logic for specifying and reasoning about concurrent and reactive systems. See also Tools for TLA project.

  86. TPS and ETPS, the Theorem Proving System and the Educational Theorem Proving System.

  88. TRIO language and tools for real-time systems, based on temporal logic.

  89. TTM/RTTL framework for real-time reactive systems.

  90. UNITY, a programming notation and a logic to reason about parallel and distributed programs.

  91. UPPAAL verification and validation tools for real-time systems. Model checking and simulation with a graphical interface.

  92. 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.

  93. * VDM (Vienna Development Method). See also Overture toolset.

  94. 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.

  95. X-machines, related to finite state machines.

  96. * Z notation for formal specification.
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.

Search for formal methods links on Vivisimo.

See also FormalMethods.com. :-)

Last updated by Jonathan Bowen, Centre for Applied Formal Methods, Museophile Limited, UK, 3 June 2008.
Further information for possible inclusion is welcome.

Part of the Museophile archive. See also ProCoS resources.