* ProCoS * Virtual Library * Computing * Software Engineering * Education

Formal Methods

FM'99: World Congress on Formal Methods, (also here)
Toulouse, France, 20-24 September 1999.

Please mail J.P.Bowen@reading.ac.uk 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 available around the world on the World Wide Web (WWW), a global hypermedia system providing worldwide information. 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). 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. Algebra of Communicating Shared Resources (ACSR) 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. Algebraic Design Language, a higher-order software specification language.

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

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

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

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

  10. 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).

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

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

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

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

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

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

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

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

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

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

  21. Duration Calculus (DC), an interval logic for real-time systems, originally developed by Prof. Zhou Chaochen et al. as part of the ProCoS project. See publications and DCVALID Duration Calculus Formulae validity checker tool (based on MONA).

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

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

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

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

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

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

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

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

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

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

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

  33. JAPE (Just Another Proof Editor) by Bernard Sufrin and Richard Bornat is available via anonymous FTP. See also MacOS JAPE.

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

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

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

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

  38. LEGO proof assistant.

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

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

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

  42. MALPAS static analysis tool-set.

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

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

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

  46. * Model checking at CMU, a method for formally verifying finite-state concurrent systems. Available packages include:

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

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

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

  50. * Nuprl tool based on intuitionistic type theory.

  51. OBJ - OBJ3, 2OBJ, CafeOBJ, etc. Term rewriting.

  52. Otter, an automated deduction system.

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

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

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

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

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

  58. * RAISE language and tools from CRI, Denmark. Email raise@csd.cri.dk.

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

  60. Refinement Calculus by Ralph Back et al..

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

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

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

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

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

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

  67. STeP, the Stanford Temporal Prover.

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

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

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

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

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

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

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

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

  76. ! 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.

  77. * VDM (Vienna Development Method).

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

  79. * 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:


Last updated by Jonathan Bowen, Formal Methods and Software Engineering Group, Deparment of Computer Science, The University of Reading, 10 May 1999.
Further information for possible inclusion is welcome.

Part of the OUCL archive. Supported by ProCoS.