Formal Runtime Error Detection During Development in the Automotive Industry
summary
Module-level abstract interpretation generates a verification harness for each component, infers contracts (pre/post, array bounds, globals, init vs cyclic calls), and runs an off-the-shelf tool asre on those drivers. Results: end-to-end runs drop from days or weeks to about 12 hours aggregated, per-module runs often finish in minutes, false alarms drop while coverage rises (over 90% in one library), typical modules show 10–100 alarms with short stacks, and about 10% of alarms lead to actual code changes.
AI-written summary · about
chapters (13)
- 0:00Abstract interpretation intro
- 1:06Functional safety in automotive
- 2:32Late-stage error detection
- 3:56Module abstraction with contracts
- 5:46Verification harness generation
- 7:15Verification driver structure
- 9:04Contract types and benefits
- 11:11Automated contract inference
- 12:15Results on automotive code
- 13:42Performance in large projects
- 15:33Developer feedback on contracts
- 16:39Conclusion and future plans
- 17:06Q&A
related talks
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
15mOn the Impact of Formal Verification on Software Development
22mTowards Modelling and Verification of Coupler Behaviour in Climate Models
45mRV: where are we?
42mHow To Make Formal Methods A Software Quality Solution That Can Actually Be Used In The Industry
42mContemporary Automatic Program Analysis
18mRISC-V Spotlight: Improving RISC-V Quality with Verification Standards and Advanc...
16mTermination Analysis for Evolving Programs: An Incremental Approach by Reusing Certified Modules