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:
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.
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.
Action Semantics, a framework for specifying formal semantics
of programming languages.
Alloy Constraint 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.
Autofocus for specifying distributed systems.
First prize winner in the tool competition at
FM'99.
Circal (CIRcuit CALculus) System supporting a process algebra which
may be used to rigorously describe, verify and simulate concurrent
systems.
See
software.
Coq proof assistant:
checks proofs about assertions,
helps to find formal proofs and
extracts certified programs from constructive proofs.
COSPAN (COordinated SPecification ANalysis),
a general-purpose rapid-prototyping tool,
using the S/R (selection/resolution) language.
See newer commercial
FormalCheck model checker.
CSP (Communicating Sequential Processes) including the
FDR2 (Failures-Divergence Refinement) tool.
FormalCheck model checker tool
for verifying the functionality of
digital hardware designs in Verilog or VHDL,
based on the
COSPAN
model checker.
HOL mechanical theorem proving system, based on
Higher Order Logic.
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.
IMPS, an Interactive Mathematical Proof System intended to provide
mechanical support for traditional mathematical techniques and styles
of practice.
Isabelle, a generic theorem prover, supporting
higher-order logic, ZF set theory, etc.
Jape (Just Another Proof Editor).
A framework for building interactive proof editors.
JML (Java Modeling Language), a
behavioral interface specification language for
Java.
KIV (Karlsruhe Interactive Verifier).
A tool for the development of correct software using stepwise
refinement.
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.
Larch family of languages and tools supporting a two-tiered
definitional style of specification.
See especially
LP, the
Larch Prover.
LeanTAP, a tableau-based deduction theorem prover for classical
first-order logic.
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.
Murphi description language and verifier tool for
finite-state verification of concurrent systems.
Pobl.
A development method for concurrent object-based programs.
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.
SPARK secure subset of Ada, including the
SPADE static analysis toolset.
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.
TLA (Temporal Logic of Actions),
a logic for specifying and reasoning about concurrent and
reactive systems.
See also
Tools for TLA project.
TPS and ETPS, the Theorem Proving System and the Educational
Theorem Proving System.
TRIO language and tools for
real-time systems, based on temporal logic.
TTM/RTTL framework for real-time reactive systems.
UNITY, a programming notation and a logic to reason about
parallel and distributed programs.
UPPAAL verification and validation tools for real-time systems.
Model checking and simulation with a graphical interface.
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.
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.
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.
![[Formal Methods Europe (FME)]](http://www.fmeurope.org/gif/logo-kl.gif){kind=logo}
![[Centre for Applied Formal Methods (CAFM), South Bank University, London, UK]](http://www.cafm.sbu.ac.uk/cafm-logo.gif){kind=logo}
Virtual Library
