Applicable and Achievable Formal Verification
summary
Explains how industry applies formal methods to real embedded devices: mandates from IEC 61508 map verification techniques to Safety Integrity Levels, and a pragmatic three-part approach—property-based, vulnerability assessment, and standards compliance—drives work on C/assembly, interrupt‑driven smart devices and custom compilers. Lists usable tools: Coverity, CodeSonar, Facebook Infer, Astrée, CBMC/ESBMC and TLA+ for design, and gives a concrete surprise: a device analysis reporting 6,000 data races that never triggered in 30 years of field data.
AI-written summary · about
chapters (19)
- 0:00Intro
- 0:55Background
- 3:10Formal Verification (Expectation)
- 3:40Is Formal Verification For Me?
- 4:22Safety-Critical Systems
- 7:05IEC 61508 - The "Golden Boy" Safety Standard
- 8:07Case 1: End-To-End Verification
- 9:14Verifying Nuclear Power Plants
- 10:37Case 2: Smart Device Verification
- 13:55Verifying Smart Sensors
- 15:55Examples
- 16:50Vulnerability Assessment tools
- 22:04Annotated Specifications
- 23:16Stand-alone Specifications
- 24:11Design Specifications
- 26:02Property Based Approach (tools)
- 26:24Benefits of Specifications
- 27:09Now what?
- 30:59Opening a Dialogue
related talks
01h 05mSoftware and Safety
48mThe Proof Must Go On: Formal Methods in the Theater of Secure Software Development(…)
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
01h 08mProviding evidence for the security properties of hardware/software codesigns
46mRevolutionizing Automotive Software: DevSecOps, Functional Safety, and Open Source Sy...
27mAutomated Learning and Verification of Embedded Security Architectures
57mFinding, Managing, Preventing Vulnerabilities: An Automotive Perspective
46mA Maintainable, Scalable, and Verifiable SW Qualification Approach for Automotive in Linux