�ݺ�ߣ

Formal Methods:
Whence and Whither?
Prof. Jonathan P. Bowen FRSA FBCS
Emeritus Professor of Computing
London South Bank University, UK
Adjunct Professor, Southwest University, Chongqing, China
Chairman, Museophile Limited, Oxford, UK
www.jpbowen.com
LSBU create a connected and Customisable Research Experience with Cayuse

Cyber-Physical Systems – safety

Logic
Aristotle’s logic – highly influential on
Western thought.
— Aristotle (384–322 BC)
Aristotle’s Lyceum, rediscovered
in Athens (1997)
Great Ideas of
Computing Science:
from Aristotle to Euclid
– Tony Hoare (2011)
Tony Hoare - Wikipedia

Proof
• Mathematics – simple theorems, deep proofs
• Cf. software – complicated specifications &
programs, shallow proofs
Fermat’s Last Theorem (c.1637):
an + bn ≠ cn (integer n > 2)
— Pierre de Fermat (1607–1665)
Proved 358 years later by Andrew Wiles, 1994/5.
Not a timescale acceptable for software!

Early 20th century developments
• David Hilbert (1862–1943)
– German mathematician and philosopher of mathematics
– 23 mathematical problems (1902)
– Hilbert’s programme: finite, complete, consistent axioms (1920s)
– Entscheidungsproblem – decision problem (1928)
• Kurl Gödel (1906–1978)
– German logician, mathematician, and philosopher
– completeness/incompleteness theorems (1929–1931)
• Alan Turing (1912–1954)
– English mathematician, computer scientist, logician, and philosopher
– Turing machines; Entscheidungsproblem unsolvable (1936)

First formal methods paper?
Checking a Large Routine, Paper for the EDSAC Inaugural
Conference, 24 June 1949. In Report of a Conference on High Speed
Automatic Calculating Machines, pp 67–69.
Reprinted with corrections and annotations in:
An early program proof by Alan Turing, L. Morris and C.B. Jones, IEEE Ann. Hist.
Computing 6(2):129–143, 1984.
See also: Turing and Software Verification, C.B. Jones. Tech. Report CS-TR-1441,
Newcastle University, UK, 2014.
— Alan Turing
Arguably the first “formal methods” paper ever:

Turing and program proving
• A.M. Turing, “Checking a large routine” (1949)
• F.L. Morris & C.B. Jones, An Early Program
Proof by Alan Turing, IEEE Annals of the
History of Computing, 6(2):139–143, 1984.
“assertions”
“verification”
“dashed” after states

Checking a large routine (1949)
• “In order to assist the checker, the programmer should make
assertions about the various states that the machine can reach.”
• “The checker has to verify that the … initial condition and the
stopped condition agree with the claims that are made for the
routine as a whole.”
• “He has also to verify that each of the assertions … is correct.”
• “Finally the checker has to verify that the process comes to an
end.”

Dashed variables
for after states

Modernized flow diagram, with assertions

Mathematics and programming
In 1951, Christopher Strachey wrote a letter to
Alan Turing on his programming plans:
“... once the suitable notation is decided, all that
would be necessary would be to type more or
less ordinary mathematics and a special
routine called, say, ‘Programme’ would convert
this into the necessary instructions to make the
machine carry out the operations indicated. This
may sound rather Utopian, but I think it, or
something like it, should be possible …”
Computer Pioneers - Christopher Strachey

Turing’s influence on program proving
• Aad van Wijngaarden was at the Cambridge meeting –
but no known influence (1949…)
• Robert Floyd rediscovered ideas similar to those of Turing
(published 1967)
• Tony Hoare developed these further (published 1969)
• Had Turing lived longer, perhaps formal methods (in
particular program proving) would have developed more
rapidly, rather than being rediscovered

Turing and
program
proving
F.L. Morris & C.B.
Jones (1984), An
Early Program
Proof by Alan
Turing, IEEE
Annals of the
History of
Computing,
6(2):139–143.
1947
1949
1963
1976
1967
1969
1966

Assertions
An Axiomatic Basic for Computer Programming.
Communications of the ACM, October 1969
— Sir Tony Hoare (b.1934)
[Photograph]
Hoare logic: {pre} prog {post}
Program proving with pre- and post-conditions as
“assertions” (logical statements about the program)
30 years later … assertions widely used by programmers
for testing and debugging rather than proof

Formal Methods:
An Introduction to Symbolic Logic
and to the Study of Effective
Operations in Arithmetic and Logic
(1962)
Evert Willem Beth (1908–1964),
Dutch philosopher and logician
Earliest book with
“formal methods”
in the title?

Formal methods
• Term established by late 1970s
– Next stage from structured design
– Mathematical basis
• Formal specification and (optionally) proof:
– Validation (correct specification)
– Verification (correct implementation wrt spec.)
• But engineers calculate rather than prove
undefined
undefined

Some formal methods approaches
• Abstract Interpretation: approximating program behaviour
to prove correctness or detect errors.
• Model-Based Testing: generating test cases from a formal
model.
• Model Checking: exhaustively verifying system behaviour
against a formal specification.
• Proof Assistants: tools for interactively constructing and
verifying mathematical proofs.
• Refinement: systematically refining a high-level
specification into a correct implementation.
• Static Analysis: analyzing program code meaning to
detect errors or enforce constraints.
• Verification: proving the correctness of a program using
logical inference rules.
2019
2019

Formal methods levels
0. Formal Specification:
– Requirements only
– No analysis or proof
– Can be used to aid testing
– Cost-effective
1. Formal Verification:
– Program produced in a more formal way
– Use of proof or refinement based on a formal specification
– More costly
2. Theorem Proving:
– Use of a theorem prover tool
– Formal machine-checked proofs
– Proof of entire system possible but scaling difficult
– Expensive and hard
2022

Formal specification
1. A specification written and
approved in accordance
with established standards
2. A specification written in a
formal notation, often for
use in proof of correctness.
— IEEE glossary

ProCoS: Provably Correct Systems
• Requirements
• Specification
• Design
• Programming
• Compilation
• Hardware
European projects and Working Group (early 1990s)
}Oldenburg
} Lyngby
} Kiel
} Oxford

Levels of abstraction/complexity
• 15k lines of (informal) requirements
• 150k lines of (formal?) specification
• 1.5 million lines of design description
• 15 million lines of (formal!) high-level program code
• 150 million machine instructions of object code
• 1.5 billion transistors in hardware!
The later a mistake is detected, the more costly it is!

ProCoS Working Group
University of Reading, UK, 1997
A ProCoS-WG Working Group Final Report: ESPRIT Working Group 8694,
Jonathan P. Bowen, C.A.R. Hoare, Hans Langmaack, Ernst-Rüdiger Olderog and Anders P. Ravn.
Bulletin of the European Association for Theoretical Computer Science, 64:63–72, February 1998.
C:UsersJonathanAppDataLocalMicrosoftWindowsTemporary Internet
FilesContent.IE58PADLV2LMC900432679[1].png

Applications of Formal Methods
Examples:
• Tektronix (Z) – oscilloscopes
• STV algorithm (VDM) – voting
• IBM CICS (B) – transaction processing
• AAMP5 microprocessor (PVS) – hardware
• GEC Alsthom (B) – railway software
• A300/340 (Z) – airplane software
Prentice Hall, International Series in Computer Science,
1995

Seven Myths of Formal Methods
1. Formal Methods can
guarantee that software is
perfect.
2. Formal Methods are all about
program proving.
3. Formal Methods are only
useful for safety-critical
systems.
4. Formal Methods require highly
trained mathematicians.
5. Formal Methods increase the
cost of development.
6. Formal Methods are
unacceptable to users.
7. Formal Methods are not used
on real, large-scale software.
– J.A. Hall, IEEE Software,
September 1990

Software Specification Methods
Using a selection of formal methods:
Z, SAZ, B, OMT, Action Systems,
UML, VHDL, Estelle, SDL, E-LOTOS,
JSD, CASL, Coq, Petri Nets.
Marc Frappier & Henri Habrias (eds.)
Springer-Verlag, FACIT series, 2001
The process of producing a formal
specification…

Education
• Resistance by students
• Resistance even by
academics
• Support by professional
societies (e.g., BCS
accreditation)

Choosing a formal method – difficult

Standards mandating formal methods
• In highest level of safety and security applications
• From 1990s*
• Also, for formal notations themselves...
* See:
Bowen, J.P. & Stavridou, V.
(1993), Safety-critical systems,
formal methods and standards.
Software Engineering Journal,
8(4):189–209. DOI:
10.1049/sej.1993.0025

Example: Z Standard
• ISO/IEC 13568
– Long process (1990s)
– Inconsistencies found!
• Final Committee Draft
– accepted in 2001
• May help tools & industrial application
http://web.comlab.ox.ac.uk/oucl/research/groups/zstandards/images/zed.gif

Theory and practice
“It has long been my personal view that the
separation of practical and theoretical work is
artificial and injurious. Much of the practical work
done in computing, both in software and in hardware
design, is unsound and clumsy because the people
who do it have not any clear understanding of the
fundamental design principles of their work. Most of
the abstract mathematical and theoretical work is
sterile because it has no point of contact with real
computing.”
— Christopher Strachey (1916–1975)
Computer Pioneers - Christopher Strachey C:UsersJonathanAppDataLocalMicrosoftWindowsTemporary Internet

How Important is mathematics to the
software practitioner?
Some consider it unimportant … !
— Robert L. Glass, IEEE Software, Nov./Dec. 2000
Some consider it important …
— William W. McMillan et al., Letters
IEEE Software, Jan./Feb. 2001
The debate has continued …

Case study:
European
airspace
European Court
of Auditors
(2017)
My flights!
London
Amsterdam
Bremen

National Air Traffic Services, UK
www.nats.co.uk
File:Nats logo 2006.png
Swanwick
southern England
Air Traffic Control (ATC) for England and Wales
• A large safety-related cyber-physical system!
iFACTS – Interim Future Area Control Tools Support
• Electronic flight strips and prediction aids
• Functional specification – Z notation
(thousands of pages – used for testing)
• Algorithm specification – Mathematica
• HMI specification – state tables
• Rest – English!

Use in industry
• Formal methods are applicable
across the lifecycle
• Engineer training not a barrier
• Tool support essential
• iFACTS in operation from 2011
– 18 minutes of prediction UK airspace

Subsequent iFACTS developments
• Traffic Load Prediction Device (TLPD):
– Forecast air traffic load up to 4 hours ahead
– Plan workloads for optimum traffic flows
• iFACTS – winner of the Duke of Edinburgh Navigation
Award for Technical Achievement (2013)
• MoD use for military air traffic control (2014)
• FourSight, successor to iFACTS (announced 2017)
for Swanwick/Prestwick – European SESAR compliant

SETSS: Engineering Trustworthy
Software Systems – education
• Annual Spring School at Southwest University,
Chongqing, China
• Held 2014–2019, restarted after COVID in 2024
• Week-long tutorials by international experts, for
graduate students from China and elsewhere
• Tutorial proceedings in Springer LNCS
• State of the art in formal methods & related research
• Cf. annual Marktoberdorf Summer School in
Germany (last held 6–17 August 2024)

SETSS
15–21 April 2024
• Seven tutorials over 5 days
• Workshop over 2 days
www.rise-swu.cn/SETSS2024

SETSS 2024 tutorials
• Zhiming Liu: Introduction to Mathematical Logic and Logic of Programming
• Cláudio Gomes: Introduction to and Deployment of Digital Twins
• Jean-Pierre Talpin: Theories of Contracts and Their Applications
• Martin G. Fränzle: AI Components for High Integrity, Safety-Critical Human-
Cyber-Physical Systems: Chances and Risks
• Moshe Y. Vardi: What Came First, Mathematics or Computing?
• Youcheng Sun: Software Engineering for Explainable AI
• Kuldeep Meel: Distribution Testing: The New Frontier for Formal Methods

Formal Methods and AI – questions
Explainable AI, etc. C:UsersJonathanAppDataLocalMicrosoftWindowsTemporary Internet

Formal methods and correctness
Rigorous specification C:UsersJonathanAppDataLocalMicrosoftWindowsTemporary Internet

AI
–
large
“learned”
models
“Correct by construction” vs. AI “dog trained” C:UsersJonathanAppDataLocalMicrosoftWindowsTemporary Internet

Formalized
mathematics
Precise language,
correctness checkable
by proof assistants

Machine
learning
Human intuition
combined with AI
Moshe Vardi

Next
SETSS
School
17–23 May 2025
Beijing, China
SETSS 2024 proceedings
• Springer LNCS volume 15884 (2025)
• https://link.springer.com/book/9789819646555
SETSS 2024 front cover:
Busts of Alan Turing and
John von Neumann at
Southwest University,
Chongqing, China

Predictions dangerous
“ . . . these formal methods are the key to writing much
better software. Their widespread use will revolutionise
software writing, and the economic benefits will be
considerable – on a par with those of the revolution in
civil engineering during the last century.”
— Brian Oakley (1927–2012),
Alvey Achievements, June 1987
Computer Resurrection Issue 60
Compare AI!

The Flat Earth Society
Cf. formal methods community…
— Gerard J. Holzmann

Unified theory? Cf. physics
“The construction of a single mathematical model
obeying an elegant set of algebraic laws is a significant
intellectual achievement; so is the formulation of a set of
algebraic laws characterising an interesting and useful
set of models.”
— Sir Tony Hoare, 1993
[Photograph]
Operational, Denotational, Algebraic semantics

Unifying Theories
of Programming
• Tony Hoare & Jifeng He
• Prentice Hall, 1998
• http://www.unifyingtheories.org
A book with a red and blue cover
Description automatically generated
• UTP international symposium
• First symposium 2006, UK
• Springer LNCS proceedings C:UsersJonathanAppDataLocalMicrosoftWindowsTemporary Internet

Future developments – whither?
• Safety-critical cyber-physical systems
• Security (e.g., smartcards, smartphones)
• Harmonization of engineering practices
• Published practical experience
• Assessment and measurement
• Technology transfer investment
• Use with AI, LLMs, etc… perhaps most promising!C:UsersJonathanAppDataLocalMicrosoftWindowsTemporary Internet

Formal methods vs. AI
Google Ngram Viewer
Japanese Fifth
Generation project
ProCoS
project!
1950–2010

Formal methods vs. AI
Google Ngram Viewer
LLMs
ChatGPT
…
2010–2022

Mathematical discoveries from program
search and large language models
Nature, vol. 625,
pp. 468–475 (2024)
nature.com/articles/s41586-023-06924-6
• Prospect: AI could suggest
outline proofs with human
interactive help for detail
• Could this approach work for
program generation/proof?

The Potential for AI in
Science and Mathematics
Science Museum, London, 17 July 2024
(c/o Oxford Mathematics)
— Terence Tao FAA FRS,
UCLA (b. 1975)
2006 Fields Medalist
Oxford Mathematics London Public Lecture: The Potential for AI in Science and Mathematics - Terence Tao. SOLD OUT | Mathematical Institute
Terence Tao - Wikipedia
youtube.com/watch?v=_sTDSO74D8Q

Maths Olympiad proof vs. arithmetic
Proof tools reliable vs. LLMs unreliable

Verify AI mathematical output
Reliable proof tools vs. unreliable LLMs

(c/o Oxford Mathematics) …maths …and also programs?
Use AI to fill in maths proof steps… …for program proofs too?
Proof assistants for formalization

ChatGPT
Give me a quotation on formal methods and artificial intelligence.
Here’s a quote on formal methods and artificial intelligence:
“Formal methods provide the rigor necessary to ensure that artificial
intelligence systems are not only functional but also reliable and
safe. Without the foundation of formal verification, the complexity
and unpredictability of AI could lead to unintended consequences.”
This highlights the crucial relationship between formal methods, which
provide structured and mathematically sound techniques for system
verification, and AI, where ensuring correctness is essential.
ChatGPT - Wikipedia
I think we are safe for the moment!

Hans Langmaack – Kiel students
Name Year Descendants
Simon, Friedemann 1978
Olderog, Ernst-Rüdiger 1981 22
Wagner, Franz 1982
Steffen, Bernhard 1987 28
Lang, Hans-Werner 1990
Buth, Karl-Heinz 1994
Buth, Bettina 1995
Müller-Olm, Markus 1996 3
Fränzle, Martin 1997 23
Weber-Wulff, Debora 1997
Mathematics Genealogy Project
Tree
ProCoS
project

Martin Fränzle – whence?
(Dr. rer. nat., Universität zu Kiel, 1997)
Dissertation: Controller Design from Temporal Logic:
Undecidability Need Not Matter
• Hans Langmaack (Dr. rer. nat., Münster, 1960)
• Heinrich Adolph Behnke (Dr. phil., Hamburg, 1923)
• Erich Hecke (Ph.D., Göttingen, 1910)
• David Hilbert (Ph.D., Königsberg, 1885)
Tree
“great great grandfather”

David Hilbert
• Ferdinand von Lindemann (Erlangen-Nürnberg, 1873)
– transcendantal numbers
• Felix Klein (Bonn, 1868)
– Klein bottle
• Julius Plücker (Marburg, 1823)
– winner of the 1866 Royal Society Copley Medal for
“analytical geometry, magnetism, & spectral analysis”
• Christian Ludwig Gerling (Göttingen, 1812)
– geodetic triangulations
• Carl Friedrich Gauß (Helmstedt, 1799)
– mathematician, astronomer, geodesist, and physicist
Tree

Carl Friedrich Gauß
• Johann Friedrich Pfaff (Göttingen, 1786)
– “Pfaffian” systems, also advisor of August Möbius
• Abraham Gotthelf Kästner (Leipzig, 1739)
– textbooks & encyclopedias, Fellow of the Royal Society
• Christian August Hausen (Halle-Wittenberg, 1713)
– electrical phenomena
• Johann Christoph Wichmannshausen (Leipzig, 1685)
– philology & philosophy
• Otto Mencke (Leipzig, 1665)
– founder of Acta Eruditorum, first German scientific journal
Tree
Möbius strip

Otto Mencke
• Jakob Thomasius (Leipzig, 1643 )
– also advisor of Gottfried Wilhelm Leibniz
• Friedrich Leibniz (Leipzig, 1739)
– father of Gottfried Wilhelm Leibniz
Tree
Binary arithmetic by Gottfried Leibniz

David Hilbert – 2nd advisor
• Heinrich Martin Weber (Heidelberg, 1866)
1. Otto Hesse (Königsberg, 1840) – mathematician
2. Robert Bunsen (Göttingen, 1831) – chemist
3. Gustav Robert Kirchhoff (Königsberg, 1840)
– chemist, mathematician, and physicist
Tree
Bunsen
burner
Kirchhoff’s
circuit laws

Abraham Gotthelf Kästner, FRS – students
• Georg Christoph Lichtenberg (Göttingen, 1769)
– German physicist and Anglophile
• Johann Friedrich August Göttling – German chemist
• Justus von Liebig – German chemist, many students
• Sir Benjamin Collins Brodie, 2nd Baronet, FRS
– English chemist; Oxford, England & Giessen, Germany
• Augustus George Vernon Harcourt, FRS (Oxford)
– English physical chemist
• Sir John Conroy, 3rd Baronet, FRS (Oxford)
• Sir Harold Hartley, FRS (Oxford)
• E. J. Bowen, FRS (DSc, Oxford)
The Academic Family Tree – https://academictree.org
Kästner crater
… & Alice Bowen! (Oxford)
(“grandfather”
of Gauß)

Einstein in Oxford
• Recent book
• Einstein Blackboard in the History of
Science Museum, Oxford
• 1931 lectures by Einstein at Rhodes
House in Oxford
• See page 12 of the book!
Happy Birthday Martin!

�ݺ�ߣ

Formal Methods: Whence and Whither? [Martin Fränzle Festkolloquium, 2025]

Recommended

More Related Content

More from Jonathan Bowen (8)

Recently uploaded (20)

Formal Methods: Whence and Whither? [Martin Fränzle Festkolloquium, 2025]