Formal methods

Virtual Library

---

Computing

---

Software engineering

---

Formal methods

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:

• Announcement
• Selected resources
• Introductory articles
• Individual notations, methods and tools
• Publications (journals, papers, books, etc.)
• Electronic repositories
• Education resources
• Meetings
• Projects
• Companies
• Organizations
• Who's who
• Selected photographs
• Newsgroups and mailing lists
• Safety-critical systems
• Related topics

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.

• Formal Methods authors on Google Scholar↑. (30 November 2011)
• Wikified and moved to formalmethods.wikia.com. (10 March 2009)
• Formal methods entries in the Wikipedia encyclopedia (30 October 2005)
• The preferred and stable URL for the Virtual Library formal methods pages is now http://vl.fmnet.info. (30 November 2004)
• Checked and updated main links to formal methods. (22 April 2001)
• Moved to the Centre for Applied Formal Methods, [http://www.lsbu.ac.uk/ London South Bank University↑. (13 January 2001)
• New education resources section by Kathi Fisler added. (23 February 1999)
• Search for newsgroup articles on formal methods in Google Groups. (19 December 1997)
• Some Formal Methods Humour. (25 September 1997)
• FM'99: The World Congress on Formal Methods, 20-24 September 1999. (24 July 1997)
• Photographs from the 1st B Conference, Nantes, France, 25–27 November 1996. (6 December 1996)
• Strategic Directions in Computing Research Formal Methods Working Group, ACM, USA. (16 September 1996)
• B-Core (UK) Ltd are now on-line. (25 June 1996)
• EVES and Z/EVES are now available for on-line distribution. (25 June 1996)
• The Steam Boiler Control Specification Problem by J.-R. Abrial, E. Börger and H. Langmaack. A comparative case study for different formal techniques. Published as LNCS 1165. (2 August 1995)
• Comp.specification.misc newsgroup. (12 July 1995)
• Petri Nets graphical notation. (11 April 1995)
• Tools demonstration information for WIFT95 workshop. (6 April 1995)
• A new LOTOS page. (16 February 1995)
• Information on RAISE language and tools. (19 January 1995, updated 17 August 1999)
• A new section on the B-Method has been added. (6 January 1995)

---

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:

• Formal methods entry and category in the Wikipedia free online encyclopedia.
• Formal Methods Europe (FME) HUB.
• Formal Methods Education Resources: Tool Pages.
• Formal Verification Methods and Tools from the VERIMAG research group, France.
• Formal verification Tools list from David Mentre, Association Gulliver.

Newsgroups and mailing lists

• Comp.specification.misc newsgroup including discussion of formal specification and methods, and other related newsgroups (see comp.specification newsgroups and here if you have news access problems):
  • Comp.specification.larch — more specific discussion on the Larch, now an archive.
  • Comp.specification.z — more specific discussion on the Z and related notations. See monthly FAQ message (Frequently Asked Questions).
• Comp.software-eng — general discussion on software engineering, including formal aspects. See also the comp.software-eng Software Engineering Archives and FAQ message information especially formal specification.
• News.announce.conferences — announcements of conferences including many specifically on formal methods or with a formal methods content; e.g., see separate page on meetings.
• Search for newsgroup articles on formal methods in Google Groups.

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

• ProCoS mailing list. FMnet, maintained by Jonathan Bowen.
• ProCoS mailing list. Provably Correct Systems, maintained by Jonathan Bowen.

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:

• Concurrent systems
• Logic programming
• Safety-critical systems
• Computational logic
• BNF (Backus-Naur Form notation)
• Formal Methods from BRICS
• Some Formal Methods Humor
• David Crocker's Formal Verification blog
• Words expressing abstract relations from Roget's Thesaurus — could be useful in describing formal specifications!
• Theory of computation sites and other computing sites
• Formal Methods links from Links2Go
• UML (Unified Modeling Language) — see also:
  • Resource page from OMG (Object Management Group)
  • 2U Consortium (Unambiguous UML)
  • pUML (Precise UML group)
  • Google Directory links
• Statecharts by David Harel
• Synchronous Applications, Languages and Programs
• TPTP Thousands of Problems for Theorem Provers
• Logical frameworks
• Cleanroom Software Engineering
• Automated reasoning systems (see also systems developed in Germany)

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.