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
newsgroup, or the newer
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.
The Steam Boiler Control Specification Problem
by J.-R. Abrial, E. Börger and H. Langmaack.
A comparative case study for different formal techniques -
further submissions are invited.
(2 August 1995)
ASLAN, a specification
language processor/proof obligation generator (email Dick Kemmerer on
kemm@cs.ucsb.edu for
further details), and GIL, a
graphical interval logic tool (email Laura Dillon on dillon@cs.ucsb.edu
for further details), are
available from a formal support tools archive (see the index) at UC Santa Barbara.
HyTech is an automatic tool for the analysis of embedded systems.
It computes the condition under which a linear hybrid system satisfies
a temporal-logic requirement. Installation requires a Mathematica
license.
IMPS, an Interactive Mathematical Proof System intended to provide
mechanical support for traditional mathematical techniques and styles
of practice.
ProofPower is a commercial tool, developed and marketed 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.
PVS (Prototype Verification System) tool based on classical typed
higher-order logic developed at the
SRI International Computer Science
Laboratory.
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
CSML and MCB, a language for compositional
description of
finite state machines and a (non-symbolic) model checker for CTL,
a
BDD library with extensions for sequential verification, and
papers on various related topics.
SPIN is an automated verification tool (model checker), using a
language based on CSP, for finite state systems, such
as protocols or validation models of distributed systems, developed at
AT&T Bell Labs.