How to Rebuild Lost Trust? Control, Promises and OpenJML
summary
A case study of a 3.5-hour intern bank app shows a transfer bug where balances drift without crashes; using OpenJML (Java Modeling Language) the bug was reproduced from crafted input and traced to a hidden long integer overflow. Applying OpenJML required adding explicit JML invariants — nonnegative balance, an upper bound, public getters, and that source and destination accounts are distinct — and the tool can statically prove correctness when the specification is complete or emit unprovable warnings to guide repairs. The talk notes OpenJML helps improve design and tests but is limited by spec quality and Java feature support and does not replace testing or design work.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 6:36Trust issues in software
- 13:42Control vs trust in code
- 24:07Contract specs over tests
- 28:39OpenJML formal verification
- 34:24Bank transfers case study
- 49:20Pros and cons of approach
- 52:12Summary and call to experiment
related talks
40mA practical approach to Java Memory Model
56mThe Anatomy of Java Vulnerabilities
45mA Healthy diet for your Java application
25mLiquidJava:Catch Bugs at Compile Time with Liquid Types
45mJava Memory Consistency Model
14mScalability and Precision by Combining Expressive Type Systems and Deductive Verification
58mPractical Java Problem Solving: A Hands-On Guide to Debugging
59m5 tips to make your Java apps more awesome. Non-functional Requirements Exemplified