Keynote: Formal Verification? No, Formal Reasoning!
summary
Argues that formal methods are more useful as formal reasoning than full verification and shows practical tactics: pick one transaction, model states as Mealy models (state+input→next state), use swimlanes to spot blind spots, and write specs before expensive tests. Recommends starting with TLA+ (good for concurrency) and Alloy for access-policy/schema checks, warns against blanket code generation, cites a 2019 outage caused by a removed garbage-collection step that a spec could have revealed, and describes a pet language for system-dynamics modeling.
AI-written summary · about
chapters (8)
- 0:0002:46 - Intro
- 2:4705:08 - Formal Methods
- 5:0911:07 - Verifying Hardware and Software
- 11:0812:47 - Strengths and Weaknesses of Verification
- 12:4822:56 - Some Problems Modelling Systems
- 22:5728:08 - Code Generator
- 28:0933:23 - Formal Reasoning and Testing
- 33:2445:37 - QnA
related talks
15mOn the Impact of Formal Verification on Software Development
42mHow To Make Formal Methods A Software Quality Solution That Can Actually Be Used In The Industry
03mInterview
23mSpecifying and Verifying Future Conditions
01h 05mVerifying Infinitely Many Programs at Once
01h 02mLanguage Design meets Verifying Compilers
17mReasoning about External Calls
28mGradual Verification: Assuring Software Incrementally