Even well-tested software like Java's JDK can have critical bugs, such as the famous integer overflow in binary search, demonstrating the limits of unit testing.
Formal methods are mathematically rigorous techniques for specifying, designing, and verifying software systems, used by organizations like NASA to ensure correctness.
Common tools like standardized flowcharts and static type systems in languages like TypeScript are practical examples of formal methods already in use.
Formal verification involves creating a mathematical proof that a software implementation correctly adheres to its formal specification, going beyond simple testing.
Building a Central Bank Digital Currency (CBDC) requires a higher level of assurance than testing can provide to prevent financial loss or money duplication.
The Isabelle proof assistant is used to model financial operations and mathematically prove that properties like the total money supply remain constant.
A practical approach involves prototyping new, high-risk features in Isabelle to find design flaws before committing to a full implementation in languages like Go.
The discussion covers the challenges of writing complete specifications, deriving programs from them, and why even a partial specification is better than none.
23:03Anja Kunkel
28:12Luise Freese
19:36Onur Kasimlar
43:07Golo Roden
56:49Jens Happe
58:19Michael Koppmann
31:13Stefan Baumgartner
27:27Christian Seifert
Jobs that call for the skills explored in this talk.
Think-cell
Foster City, United States of America
Saby New Compy
Karlsruhe, Germany
Vesterling Consulting GmbH
Vesterling Consulting GmbH
Vesterling Consulting GmbH
Vesterling Consulting GmbH