Glossary

ADT

 
Abstract Data Types (initial algebra specification, etc)

AL

 
Algorithms and Complexity

ARef

 
Algorithm refinement, loop invariants, implicit/explicit specs, etc

AS

 
Action Semantics

ASM

 
Abstract State Machines

ASe

 
Algebraic Semantics

ATP

 
Automated theorem proving

AbsI

 
Abstract Interpretation

Actress

 
Actress system for action semantics

Alloy

 
Alloy

AoP

 
Algebra of Programming, relational calculus

AtelierB

 
Atelier-B

B

 
B-Method

BDD

 
Binary decision diagrams

BDDC

 
BBDC - a basic BDD calculator

Btlk

 
B-Toolkit

CADP

 
CADP (Caesar/Aldebaran Development Package)

CADiZ

 
Computer Aided Design in Z

CASL

 
The Common Algebraic Specification Language

CCS

 
Calculus of Communicating Systems

CSP

 
Communicating Sequential Processes

CTL

 
Computation Tree Logic

CWB

 
The Edinburgh Concurrency Workbench

CommUnity

 
CommUnity

Coq

 
The Coq proof assistant

DMat

 
Discrete Maths (ZF set theory, functions, relations, lattices, fixpoints, graphs etc)

DRef

 
Data refinement

ELotos

 
Enhanced LOTOS

ESCJava

 
Extended Static Checker for Java

Estelle

 
Estelle

FDR

 
Failures-Divergence Refinement

FOL

 
First-Order Logic

FP

 
Functional Programming

FPT

 
Formal program techniques: pre-/post-conditions, invariants, proofs, verification, etc

FS

 
Formal Semantics (operational, axiomatic, denotational etc)

FSP

 
Finite State Process

FixP

 
Fixed Point Calculus

FuZZ

 
FuZZ printing/type-checking system for Z specifications

GHC

 
Glasgow Haskell Compiler

Gofer

 
Gofer

HL

 
Hoare Logic

HOL

 
HOL Theorem Proving system

Haskell

 
Haskell

Hugs

 
Hugs

INA

 
Integrated Net Analyzer

IVDM

 
Irish School of VDM

IVDMH

 
Irish VDM Haskell Library

Isabelle

 
Isabelle

JML

 
Java Modeling Language

LOTOS

 
LOTOS

LTL

 
Linear Time Temporal Logic

LTSA

 
Labelled Transition System Analyser

LamC

 
(Typed) Lambda Calculus

Lotrec

 
Lotrec tableaux theorem prover

MC

 
Model Checking

MPC

 
Mathematics of Program Construction (inc algorithmic problem solving, algebra, category theory)

MPS

 
Specification paradigms and integration concerns, multi-paradigm specifications, etc

MSC

 
Message Sequence Charts

NuSMV

 
NuSMV

OZ

 
Object-Z Specification Language

Ocaml

 
The CAML Language

PA

 
Process Algebras and Calculi, LTS, etc

PEP

 
Programming Envirohent based on Petri Nets

PV

 
Program verification

PVS

 
The PVS Specification and Verification System

Petri

 
Petri Nets

PiC

 
Pi-Calculus

PicT

 
PICT

PolyT

 
Polytypism and genericity

Prolog

 
Prolog

RAISEtools

 
RAISE tools

RAT

 
Recife Action Tools

RC

 
Refinement Calculus

RML

 
Relational Meta-Language system for natural semantics

RSL

 
RAISE Specification Language

RefB

 
Refinement in B

SA

 
Software architecture

SDL

 
SDL (Spec. and Desc. Language)

SML

 
The Standard ML Programming Language

SPIN

 
SPIN

Safety

 
Safety Analysis Techniques

ScTD

 
Scott Theory of Domains

TFM

 
Software Testing

TL

 
Temporal Logic

TLA

 
The Temporal Logic of Actions

TRIO

 
The TRIO/PVS tool

TT

 
Type theory

TrL

 
Trusted Logic

UPPAAL

 
UPPAAL

Unity

 
Unity

VDMSL

 
VDM ISO Standard Language

VDMT

 
IFAD VDMTools

VPP

 
VDM++

WHY

 
Why - a software verification tool

Z

 
Z-Notation

ZANS

 
Z Animation Tool

ZEVES

 
Z/EVES

ZTC

 
Z Type Checker

xML

 
Extended ML