Point of contact
Virgile Prevosto, CEA List
Summary
Formal verification is usually understood as taking place in a traditional V development cycle, i.e., occurring at a late stage, over stable and mature code. This goes against newer practices (DevOps). Letting software analyzers scale to whole software repositories and offer incremental results when launched over successive revisions of the same components is an important challenge in this respect.
A few references
- O’Hearn, P. W. Continuous Reasoning: Scaling the impact of formal methods. ACM/IEEE Symposium on Logic in Computer Science. 2018
- Zeller, M., Ratiu, D., Rothfelder, M., & Buschmann, F. An Industrial Roadmap for Continuous Delivery of Software for Safety-critical Systems. International Conference on Computer Safety, Reliability and Security (SAFECOMP). 2020