Formal verification with AI
| Reference number | |
| Coordinator | Prover Technology AB |
| Funding from Vinnova | SEK 1 712 432 |
| Project duration | March 2019 - February 2022 |
| Status | Completed |
Purpose and goal
During the project we have developed a prototype of a tool for formal verification that uses machine learning to speed-up the analysis. The goal has been that the prototype should provide greatly improved performance. The largest performance increase has been achieved when searching for counter-models to failing safety requirements. Here a typical gain has been of the order of 5x for large systems (in some cases up to 100x). The scope of the project didn´t allow us to invest the amount of work on increased automation as we would have wanted, but it´s an important focus area for the future.
Expected results and effects
When developing the prototype, we focused on using machine learning to find better strategies for our proof engine. During the project we focused on railway and subway applications, but since the performance improvements are generic, they should work just as well in the analysis of other types of systems, such as IoT or self-driving cars. However, there was not enough time to perform any specific evaluation of these areas within the project. The project has given us good insights into how machine learning can be used to improve formal verification.
Planned approach and implementation
The project plan was reasonable, even if the work later had a more iterative character; in the middle of the project, work in all three phases took place simultaneously. Phase 1 had a larger scope than planned and many ideas needed to be tested in the prototype to find out whether they should be rejected or not. The limiting factors were (and are) mainly time and resources, and there are still a lot of ideas we want to explore in the future. The expected amount of computer resources required by the project was initially underestimated, but could still be reasonably handled during the project.