|
|
Ref.
|
Topics
|
CC2001
|
SEEK04
|
|---|
|
FOUNDATIONS |
|
FM01
|
Set-theoretic/topological foundations of Formal Methods |
|
|
DMat
|
Discrete Maths (ZF set theory, functions, relations, graphs, trees etc)
|
DS1
|
FND.mf.1,FND.mf.5
|
|
|
FixP
|
Lattice and Fixed Point Calculus
|
|
|
|
|
ScTD
|
Scott Theory of Domains
|
|
|
|
FM02
|
Logical foundations of Formal Methods |
|
|
FOL
|
First-order logic (proof techniques, etc)
|
DS2, DS3
|
FND.mf.2, CMP.fm.8
|
|
|
HL
|
Hoare Logic
|
|
|
|
|
LamC
|
(Typed) Lambda Calculus
|
|
|
|
|
TL
|
Temporal Logic
|
|
|
|
|
LTL
|
Linear Time Temporal Logic
|
|
|
|
|
CTL
|
Computation Tree Logic
|
|
|
|
|
TLA
|
The Temporal Logic of Actions
|
|
|
|
FM03
|
Type-theoretic foundations of Formal Methods |
|
|
TT
|
Type theory and type systems
|
PL9
|
|
|
|
PolyT
|
Polytypism and genericity
|
|
|
|
FM04
|
Algebraic foundations of Formal Methods |
|
|
AlS
|
Algebraic structures, initial/final algebras
|
|
FND.mf.11
|
|
|
MPC
|
Mathematics of Program Construction (inc algebra, category theory)
|
|
|
|
FORMAL SPECIFICATION PARADIGMS |
|
FM05
|
Property oriented specification |
|
ADT
|
Abstract Data Types (initial algebra specification, etc)
|
|
|
|
|
CASL
|
The Common Algebraic Specification Language
|
|
|
|
FM06
|
Model oriented specification |
|
ASM
|
Abstract State Machines
|
|
CMP.fm.2
|
|
FPT
|
Formal program techniques: pre-/post-conditions, invariants, proofs, verification, etc.
|
SE10
|
MAA.md.2
|
|
B
|
B-Method
|
|
CMP.fm.2
|
|
|
VDM
|
Vienna Development Method
|
|
CMP.fm.2
|
|
|
VDMSL
|
VDM Standard Language
|
|
|
|
VPP
|
VDM++
|
|
|
|
IVDM
|
Irish School of VDM
|
|
|
|
RSL
|
RAISE Specification Language
|
|
|
|
OZ
|
Object-Z Specification Language
|
|
|
|
Z
|
Z-Notation
|
|
CMP.fm.2
|
|
Alloy
|
Alloy
|
|
|
|
FM07
|
Multi-paradigm specification |
|
MPS
|
Integration concerns, multi-paradigm specifications
|
|
|
|
CORRECTNESS, VERIFICATION AND CALCULATION |
|
FM08
|
Correct by construction |
|
AoP
|
Algebra of Programming, relational calculus
|
|
CMP.fm.4, EVO.ac.7
|
|
FM09
|
Correct by verification |
|
PV
|
Program verification
|
SE10
|
MAA.md.4
|
|
BDD
|
Binary decision diagrams
|
|
|
|
FM10
|
Correct by machine checking |
|
MC
|
Model Checking
|
|
MAA.md.4
|
|
ATP
|
Automated Theorem Proving
|
|
|
|
TFM
|
Testing with formal methods
|
|
|
|
FM11
|
Refinement techniques |
|
ARef
|
Algorithm refinement, loop invariants, etc
|
|
CMP.fm.6, CMP.fm.7
|
|
DRef
|
Data refinement
|
|
CMP.fm.6, CMP.fm.7
|
|
RC
|
Refinement Calculus
|
|
CMP.fm.6, CMP.fm.7
|
|
RefB
|
Refinement in B
|
|
CMP.fm.6, CMP.fm.7
|
|
FORMAL SEMANTICS |
|
FM12
|
Programming language semantics |
|
AS
|
Action Semantics
|
|
|
|
ASe
|
Algebraic Semantics
|
PL10
|
|
|
FS
|
Denotational and Operational Semantics
|
PL10
|
|
|
AbsI
|
Abstract interpretation
|
PL5
|
|
|
FM13
|
Formalizing distribution, concurrency and mobility |
|
PA
|
Process algebras
|
|
|
|
CCS
|
Calculus of Communicating Systems
|
|
|
|
CSP
|
Communicating Sequential Processes
|
|
CMP.fm.2
|
|
PiC
|
 -calculus
|
|
|
|
Petri
|
Petri Nets
|
|
|
|
FSP
|
Finite State Processes
|
|
|
|
MSC
|
Message Sequence Charts
|
|
|
|
LOT
|
LOTOS
|
|
|
|
|
ELOT
|
Enhanced LOTOS
|
|
|
|
|
Estelle
|
Estelle
|
|
|
|
SUPPORT FOR EXECUTABLE SPECIFICATION |
|
FM14
|
Declarative programming |
|
|
FP
|
Functional Programming
|
PL7
|
|
|
|
Haskell
|
Haskell
|
|
|
|
|
SML
|
The Standard ML Programming Language
|
|
|
|
|
CAML
|
The CAML Language
|
|
|
|
|
Prolog
|
Prolog
|
|
|
|
OTHER TOPICS |
|
FM15
|
|
|
|
AL
|
Algorithms and Complexity
|
AL2
|
|
|
|
SA
|
Software Architecture
|
|
|
|
|
JML
|
Java Modelling Language
|
|
|
|
|
Safety
|
Safety Analysis Techniques
|
|
|
![[*]](file:/usr/share/latex2html/icons/crossref.png){kind=icon}
).
Wherever possible, the entries in the table refer to the SEEK units
mentioned earlier on,
as well as to some of the following units of the CC2001 CS body of knowledge
(directly or indirectly) related to formal methods: