Virtual Library

Computing

Software Engineering

Education

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.

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:

• 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 index
• Selected photographs
• Newsgroups and mailing lists
• Related topics

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.

• New Duration Calculus and RAISE pages. (31 July 1999 / 17 August 1999)
• New education resources section by Kathi Fisler added. (23 February 1999)
• Search for newsgroup articles on formal methods in Deja.com. (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). See also ASM - Europe, University of Paderborn, Germany. Formerly known as Evolving Algebras.

2. ACL2 (A Computational Logic for Applicative Common Lisp) Version 1.9 theorem prover (1997), 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. Alcoa: Alloy Constraint Analyzer, based on a Z-like language for object models.

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

7. Algebraic Design Language, a higher-order software specification language.

8. Argos, an imperative synchronous language with verification support.

9. Assertion Definition Language Translator (ADLT), a specification based testing toolset.

10. BDDs (Binary Decision Diagrams) for finite-state verification problems.

11. B-Method, including the B-Tool and B-Toolkit.

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

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

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

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

16. CLaReT: The Computer Language Reasoning Tool.

17. CoFI: The Common Framework Initiative, for algebraic specification and development.

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

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

20. Coq proof assistant. See also CtCoq, a working environment for Coq.

21. COSPAN (COordinated SPecification ANalysis), a general-purpose rapid-prototyping tool, using the S/R (selection/resolution) language.

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

23. CWB (Edinburgh Concurrency Workbench) automated toolset. See also the 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.

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

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

26. Escher tool and ESEL language.

27. Estelle Formal Description Technique (IS 9074). See also EDT (Estelle Development Toolset).

28. Esterel language and tools for synchronous reactive systems, including Xeve, an Esterel Verification Environment.

29. EVES tool, based on ZF set theory, from ORA, Canada. See also Z/EVES which provides a Z notation front-end to EVES. Both are now available for on-line distribution.

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

31. FormalCheck tool for verifying the functionality of ASIC and digital IC designs in Verilog or VHDL from Bell Labs, based on the COSPAN model checker.

32. GIL, a graphical interval logic tool. See also publications by Laura Dillon).

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

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

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

36. Interval Temporal Logic (ITL). See also publications.

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

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

39. KIV (Karlsruhe Interactive Verifier). A tool for the development of correct software using stepwise refinement.

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

41. Larch and LP ( Larch Prover). See also DEC SRC's Larch Home Page and the Larch Project at CMU. The Larch tool set (look at the README file first) is available.

42. LeanTaP, a tableau-based deduction theorem prover for classical first-order logic.

43. LEGO proof assistant.

44. LOTOS (Language of Temporal Ordering Specifications). See also information from Madrid, Ottawa and Stirling.

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

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

47. MALPAS static analysis tool-set.

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

49. MathSpad structure editor, especially for mathematical calculations.

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

51. Mizar tool, a long-term effort aimed at developing software to support a working mathematician in preparing papers.

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

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

54. NP-Tools (a framework for mathematically proving safety properties), including Prover (a theorem prover for propositional logic extended with finite integer arithmetic) from Logikkonsult. Prover is also marketed by NPL in the UK.

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

56. Nuprl tool based on intuitionistic type theory.

57. OBJ - OBJ3, 2OBJ, CafeOBJ, etc. Term rewriting and algebraic specification.

58. Otter, an automated deduction system.

59. Petri Nets, a formal graphical notation for modelling systems with concurrency. See also conferences and tools.

60. Pi-calculus, a calculus for mobile processes. See also the Mobility Workbench and a searchable bibliography.

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

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

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

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

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

66. Refinement Calculus by Ralph Back et al..

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

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

69. SGM (State Graph Manipulator). A real-time model checking verification tool.

70. Signal language for synchronous systems. (Information in French.) See also the related Esterel amd Lustre.

71. SPARK secure subset of Ada, including SPARK Examiner tool for program analysis and verification.

72. SPIN is an automated verification tool (model checker), using PROMELA (Pocess 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.

73. STeP, the Stanford Temporal Prover.

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

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

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

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

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

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

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

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

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

83. VDM (Vienna Development Method).

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

85. Z notation for formal specification.

• Formal Methods Europe (FME) HUB. See databases (e.g., FME Tools Database with an index by formal language and a list of tools).

• Tools demonstration information for WIFT'95 workshop.

• Formal Verification Methods and Tools from the VERIMAG research group, France.

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.
  • 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. Messages relating to formal methods and software safety in this newsgroup have been archived. See also the comp.software-eng Software Engineering Archives and FAQ message information especially formal specification. (See here here if you do not have direct news access.)

• 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). (See here here if you do not have direct news access.)

• Search for newsgroup articles on formal methods in Deja.com.

• Comp.specification.* Frequently Mentioned Resources from People Helping One Another Know Stuff (PHOAKS). A count of and link to URLs mentioned in newsgroup articles. See also comp.software-eng resources.

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

• Educational issues relating to formal methods in computer science. Email formal-methods-request@cs.uidaho.edu to join/leave the list and formal-methods@cs.uidaho.edu to post to the list.

• FSDM mailing list. Formal Software Development Methods, maintained by the SVCR, Australia. Email fsdm@it.uq.edu.au to post to and join/leave the list.

• 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

• Automated reasoning systems (see also systems developed in Germany)
• BNF (Backus-Naur Form notation)
• BRICS Tools (a collection of automated verification tools) and Formal Methods
• Cleanroom:
  • Cleanroom Software Engineering including design and verification from IBM's Cleanroom Software Technology Center.
  • Cleanroom Software Engineering, Inc., including other sources.
  • A DoD STARS Tutorial including mathematical principles.
• Computational logic
• Concurrent systems
• Logic programming
• Logical frameworks
• Safety-critical systems
• Formal Methods Humour
• 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

Part of the OUCL archive. Supported by ProCoS.