Abstract Interpretation in Industry - Experience and Lessons Learned

on YouTube ↗01h 08m

" summary

Commercialized two abstract-interpretation analyzers: aiT WCET Analyzer for worst-case execution time and Astrée for absence of runtime errors, built at absin and validated against hardware traces. Development costs about 15–20 person‑years for early prototypes, supports 25+ target architectures, and achieves ~15% WCET overestimation on analyzed processors. On large automotive projects (3–100M preprocessed LOC) analysis runs around a day, reports ~14 definite runtime errors per MLOC and ~733 general alarms per MLOC, and directive tuning cuts alarms ~20%.

AI-written summary · about

" chapters (26)

1. 0:00Introduction
2. 1:28Company focus on abstract interpretation
3. 4:14Commercializing abstract interpretation tools
4. 6:01Worst-case execution time analysis
5. 8:09Challenges in execution time bounds
6. 9:13Tool architecture for execution time
7. 12:47Cache analysis and timing prediction
8. 15:59Fixpoint iteration in cache analysis
9. 17:20Cache analysis limitations and hardware
10. 18:43Speculative hardware and timing accidents
11. 21:10Timing analysis methodology
12. 22:14Pipeline analysis with speculative features
13. 27:05Validation and certification of tools
14. 33:49Commercializing AS3 stack tool
15. 34:54AS3 development and usability
16. 37:22AS3 initial capabilities
17. 38:05AS3 usability and automation improvements
18. 41:35AS3 for concurrent and cybersecurity
19. 43:45Automotive software integration with AS3
20. 47:40Results from automotive projects
21. 51:34Market challenges for formal methods
22. 53:24Safety norms and formal methods adoption
23. 56:16Academic research versus industry standards
24. 57:17Future challenges in software complexity
25. 58:19Conclusion and lessons learned
26. 59:48Q&A