Formal Methods: Whence and Whither? [Martin Fränzle Festkolloquium, 2025]
jpbowen
112 views
71 slides
Mar 05, 2025
Slide 1 of 71
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
About This Presentation
Alan Turing arguably wrote the first paper on formal methods 75 years ago. Since then, there have been claims and counterclaims about formal methods. Tool development has been slow but aided by Moore’s Law with the increasing power of computers. Although formal methods are not widespread in practi...
Slide Content
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, MuseophileLimited, Oxford, UK
www.jpbowen.com
LS BU crea te a connected a nd Customisa ble Resea rch Experience with Ca y use
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, MuseophileLimited, Oxford, UK
www.jpbowen.com
LS BU crea te a connected a nd Customisa ble Resea rch Experience with Ca y use
Paper
•Slides
•Slides
Paper
•Slides
•Slides
Paper
•Slides
•Slides
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 Hoa re - Wik ipedia
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 Hoa re - Wik ipedia
Proof
•Mathematics – simple theorems, deep proofs
•Cf. software – complicated specifications &
programs, shallow proofs
Fermat’s Last Theorem (c.1637):
a
n
+ b
n
≠ c
n
(integer n > 2)
— Pierre de Fermat (1607–1665)
Proved 358 years later by Andrew Wiles, 1994/5.
Not a timescale acceptable for software!
•Mathematics – simple theorems, deep proofs
•Cf. software – complicated specifications &
programs, shallow proofs
Fermat’s Last Theorem (c.1637):
a
n
+ b
n
≠ c
n
(integer n > 2)
— Pierre de Fermat (1607–1665)
Proved 358 years later by Andrew Wiles, 1994/5.
Not a timescale acceptable for software!
Early 20
th
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)
th
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:
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
•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.”
•“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.”
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.
•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.
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.
Dashed variables
for after states
•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.
Dashed variables
for after states
Turing and program proving
Modernized flow diagram, with assertions
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 S tra chey
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 S tra chey
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
•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
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)
[Photog ra ph]
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
An Axiomatic Basic for Computer Programming.
Communications of the ACM, October 1969
— Sir Tony Hoare (b.1934)
[Photog ra ph]
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?
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
•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
•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
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
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
•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!
•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: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
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: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[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
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
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
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
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
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
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
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
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…
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)
•Resistance by students
•Resistance even by
academics
•Support by professional
societies (e.g., BCS
accreditation)
Choosing a formal method – difficult
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
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
•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. comla b. ox. a c. uk /oucl/resea rch/g roups/zsta nda rds/ima g es/zed. g if
•ISO/IEC 13568
–Long process (1990s)
–Inconsistencies found!
•Final Committee Draft
– accepted in 2001
•May help tools & industrial application
http: //web. comla b. ox. a c. uk /oucl/resea rch/g roups/zsta nda rds/ima g es/zed. g if
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 S tra chey C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
“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 S tra chey C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
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 …
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
European
airspace
European Court
of Auditors
(2017)
My flights!
London
Amsterdam
Bremen
National Air Traffic Services, UK
www.nats.co.uk
F ile: Na ts log o 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!
www.nats.co.uk
F ile: Na ts log o 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
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
•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
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
•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
•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)
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
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
•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: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Explainable AI, etc.
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Formal methods and correctness
Rigorous specification
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Rigorous specification
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
AI
–
large “learned” models
“Correct by construction” vs. AI “dog trained”
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
–
large “learned” models
“Correct by construction” vs. AI “dog trained”
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Formalized mathematics
Precise language,
correctness checkable
by proof assistants
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Precise language,
correctness checkable
by proof assistants
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Machine learning
Human intuition
combined with AI
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Moshe Vardi
Human intuition
combined with AI
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
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
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 I ssue 60
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. pngCompare AI!
“ . . . 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 I ssue 60
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. pngCompare AI!
The Flat Earth Society
Cf. formal methods community…
— Gerard J. Holzmann
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Cf. formal methods community…
— Gerard J. Holzmann
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
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
[Photog ra ph]
Operational, Denotational, Algebraic semantics
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
“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
[Photog ra ph]
Operational, Denotational, Algebraic semantics
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Unifying Theories
of Programming
•Tony Hoare & Jifeng He
•Prentice Hall, 1998
•http://www.unifyingtheories.org
A book with a red a nd blue cov er
Description a utoma tica lly g enera ted
•UTP international symposium
•First symposium 2006, UK
•Springer LNCS proceedings
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
of Programming
•Tony Hoare & Jifeng He
•Prentice Hall, 1998
•http://www.unifyingtheories.org
A book with a red a nd blue cov er
Description a utoma tica lly g enera ted
•UTP international symposium
•First symposium 2006, UK
•Springer LNCS proceedings
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
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: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
•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: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Formal methods vs. AI
Google Ngram Viewer
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Japanese Fifth
Generation project
ProCoS
project!
1950–2010
Google Ngram Viewer
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Japanese Fifth
Generation project
ProCoS
project!
1950–2010
Formal methods vs. AI
Google Ngram Viewer
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
LLMs
ChatGPT
…
2010–2022
Google Ngram Viewer
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
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?
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
O xford M a thema tics London Public Lecture: The Potentia l for A I in S cience a nd M a thema tics - Terence Ta o. S O LD O UT | M a thema tica l I nstitute
Terence Ta o - Wik ipedia
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
youtube.com/watch?v=_sTDSO74D8Q
Science and Mathematics
Science Museum, London, 17 July 2024
(c/o Oxford Mathematics)
— Terence Tao FAA FRS,
UCLA (b. 1975)
2006 Fields Medalist
O xford M a thema tics London Public Lecture: The Potentia l for A I in S cience a nd M a thema tics - Terence Ta o. S O LD O UT | M a thema tica l I nstitute
Terence Ta o - Wik ipedia
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
youtube.com/watch?v=_sTDSO74D8Q
Science Museum, London, 17 July 2024
(c/o Oxford Mathematics)
The Potential for AI in
Science and Mathematics
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Maths Olympiad proof vs. arithmetic
Proof tools reliable vs. LLMs unreliable
(c/o Oxford Mathematics)
The Potential for AI in
Science and Mathematics
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Maths Olympiad proof vs. arithmetic
Proof tools reliable vs. LLMs unreliable
The Potential for AI in
Science and Mathematics
Science Museum, London, 17 July 2024
(c/o Oxford Mathematics)
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Verify AI mathematical output
Reliable proof tools vs. unreliable LLMs
Science and Mathematics
Science Museum, London, 17 July 2024
(c/o Oxford Mathematics)
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Verify AI mathematical output
Reliable proof tools vs. unreliable LLMs
The Potential for AI in
Science and Mathematics
Science Museum, London, 17 July 2024
(c/o Oxford Mathematics)
…maths …and also programs?
Use AI to fill in maths proof steps……for program proofs too?
Proof assistants for formalization
Science and Mathematics
Science Museum, London, 17 July 2024
(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.
Cha tGPT - Wik ipedia
I think we are safe for the moment!
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
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.
Cha tGPT - Wik ipedia
I think we are safe for the moment!
C: \Users\Jona tha n\A ppDa ta \Loca l\M icrosoft\Windows\Tempora ry I nternet
F iles\Content. I E5\8PA DLV 2L\M C900432679[1]. png
Hans Langmaack – Kiel students
Name YearDescendants
Simon, Friedemann 1978
Olderog, Ernst-Rüdiger198122
Wagner, Franz 1982
Steffen, Bernhard 198728
Lang, Hans-Werner 1990
Buth, Karl-Heinz 1994
Buth, Bettina 1995
Müller-Olm, Markus 19963
Fränzle, Martin 199723
Weber-Wulff, Debora 1997
Mathematics Genealogy Project
Tree
ProCoS
project
Name YearDescendants
Simon, Friedemann 1978
Olderog, Ernst-Rüdiger198122
Wagner, Franz 1982
Steffen, Bernhard 198728
Lang, Hans-Werner 1990
Buth, Karl-Heinz 1994
Buth, Bettina 1995
Müller-Olm, Markus 19963
Fränzle, Martin 199723
Weber-Wulff, Debora 1997
Mathematics Genealogy Project
Tree
ProCoS
project
Martin Fränzle – whence?
(Dr. rer. nat., UniversitätzuKiel, 1997)
Dissertation: Controller Design fromTemporal Logic:
UndecidabilityNeed 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)
Mathematics Genealogy Project
Tree
“great great grandfather”
(Dr. rer. nat., UniversitätzuKiel, 1997)
Dissertation: Controller Design fromTemporal Logic:
UndecidabilityNeed 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)
Mathematics Genealogy Project
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
Mathematics Genealogy Project
Tree
•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
Mathematics Genealogy Project
Tree
Carl Friedrich Gauß
•Johann Friedrich Pfaff (Göttingen, 1786)
–“Pfaffian”systems, alsoadvisorof 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)
–founderof Acta Eruditorum, first German scientificjournal
Mathematics Genealogy Project
Tree
Möbius strip
•Johann Friedrich Pfaff (Göttingen, 1786)
–“Pfaffian”systems, alsoadvisorof 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)
–founderof Acta Eruditorum, first German scientificjournal
Mathematics Genealogy Project
Tree
Möbius strip
Otto Mencke
•Jakob Thomasius (Leipzig, 1643 )
–alsoadvisorof Gottfried Wilhelm Leibniz
•Friedrich Leibniz (Leipzig, 1739)
–father of Gottfried Wilhelm Leibniz
Mathematics Genealogy Project
Tree
Binary arithmetic by Gottfried Leibniz
•Jakob Thomasius (Leipzig, 1643 )
–alsoadvisorof Gottfried Wilhelm Leibniz
•Friedrich Leibniz (Leipzig, 1739)
–father of Gottfried Wilhelm Leibniz
Mathematics Genealogy Project
Tree
Binary arithmetic by Gottfried Leibniz
David Hilbert – 2
nd
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
Mathematics Genealogy Project
Tree
Bunsen
burner
Kirchhoff’s
circuit laws
nd
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
Mathematics Genealogy Project
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, 2
nd
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ß)
•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, 2
nd
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!
•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?
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
LS BU crea te a connected a nd Customisa ble Resea rch Experience with Ca y use
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
LS BU crea te a connected a nd Customisa ble Resea rch Experience with Ca y use
The End
Tags
formal methods
software engineering
computer science
artificial intelligence
history of computing
cyber-physical systems
logic
proof
alan turing
program proving
mathematics
programming
assertions
formal specification
safety
abstraction
standards
air traffic control
trustworthy software
software systems
Download
Download Slideshow Get the original presentation fileQuick Actions
Statistics
- Views 112
- Slides 71
- Age 274 days
Related Slideshows
11
8-top-ai-courses-for-customer-support-representatives-in-2025.pptx
JeroenErne2
49 views
10
7-essential-ai-courses-for-call-center-supervisors-in-2025.pptx
JeroenErne2
48 views
13
25-essential-ai-courses-for-user-support-specialists-in-2025.pptx
JeroenErne2
37 views
11
8-essential-ai-courses-for-insurance-customer-service-representatives-in-2025.pptx
JeroenErne2
35 views
21
Know for Certain
DaveSinNM
23 views
17
PPT OPD LES 3ertt4t4tqqqe23e3e3rq2qq232.pptx
novasedanayoga46
26 views