-
- We list a personal selection of what we consider the major
formal methods as of June 14, 2003.
- For a more comprehensive, basically uncensored, list we refer to
``The'' Formal Methods Home
Page
The list:
- ASM:
Abstract-State Machines
- Action
Systems:
A
refinement calculus for parallel and reactive systems
- B
France, or
B
UK - for
Bourbaki
- CafeOBJ:
A rewrite logic and hidden algebra OBJ-like specification and
programming language
- CASL:
Common Algebraic Specification Language
- Coq:
A proof
assistant. Coq, as a project, has been dissolved, 2000. Now see
LOGICAL
- CSP:
Communicating Sequential Processes
- Duration
Calculi:
A continuous time interval
temporal logic
- Esterel:
Synchronous teactive programming
- HOL:
Higher Order Logic
- HyTech:
Hybrid Technology -- an automatic tool for the analysis of embedded systems
- Isabelle:
A generic theorem proving environment
- Interval Temporal
Logic
- Linear Temporal
Logic
- LSCs:
, and
Live Sequence
Charts
- LOGICAL:
Logic and computing
- Maude:
Algebraic semantics based equational and rewriting logic
specification and programming language
- MSCs:
,
and Message Sequence
Charts, or
even
this !
- Model-checking @ CMU
- Nqthm:
The Boyer-Moore prover
- nuprl:
A proof & program refinment logic.
- Petri Nets
- Pi-Calculus:
Calculi for Mobile Processes
- PVS:
Prototype
Verification System
- Refinement
Calculus
- RAISE:
Rigorous Approach to Industrial Software Engineering
- REACT: The specification, verification and
synthesis
of
concurrent, reactive, real-time and hybrid systems.
See also
STeP:
Stanford Temporal Prover.
- SpecWare
- SPIN:
On-the-fly Linear Temporal Logic Model Checking
- Statecharts
- TLA /
TLA+
Temporal Logic of Actions
- UNITY:
A programming notation and a logic to reason about parallel and distributed programs.
- UppAal:
An integrated tool environment for modeling, validation and
verification of real-time systems
- VDM:
Vienna Development Method
- Z
- for Zermelo
For a list of people closely associated with each of the above
methods, please see:
See some related Formal Methods pages:
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
Which are some major Formal Methods ?
This document was generated using the
LaTeX2HTML translator Version 2K.1beta (1.47)
Copyright © 1993, 1994, 1995, 1996,
Nikos Drakos,
Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999,
Ross Moore,
Mathematics Department, Macquarie University, Sydney.
The command line arguments were:
latex2html -split 0 -toc_depth 6 which-fms
The translation was initiated by on 2003-06-14
2003-06-14