Our model checker Prover SL CE (PSL) is getting a lot faster thanks to artificial intelligence techniques (AI)! We are now able to solve some of the hardest benchmarks in our suite in half the time, and in some cases even 10 times faster! In fact, we are not only getting faster but also more efficient, using less computer resources, in some cases only 8% of the previous ones.
How do we do that?
Well, each system is unique and can benefit from a (sometimes radically) different proof tactic. In practice, though, finding the best proof tactic can be as hard as proving the property itself. So model checkers typically ship a few pre-cooked proof tactics that work reasonably well for most problems. Our “secret sauce” is rather to learn the best proof tactic for a specific system using AI, thereby making the search process much more efficient.
These are just the first results of a significant R&D project on AI that we started in the Spring. Of course, there is still much work to do. Our goal is to develop deep-learning models that automatically propose a good proof tactic by recognizing the high-level patterns in our customers’ HLL models.
We have been following the latest achievements in the AI field with great interest, and after having been awarded R&D funds by Vinnova, Sweden’s Innovation Agency, we finally took the decision to move forward with the future of formal verification. AI is playing an increasingly important role in our society and life. Soon AI may be driving our cars and who knows what more… perhaps proving our safety properties in the blink of an eye?
Share this article
Learn to build a solid safety case for rail control systems using formal verification
Fill out your information here.
More News & Articles
Prover, RATP and Systerel publish the unified HLL 4.0 specification, keeping the rail industry's formal verification language open and free of dialects.
Generative AI has entered railway software engineering ahead of the standards governing it. A new CENELEC draft amendment to EN 50716 doesn't add requirements. It clarifies which existing rules apply when AI drafts specs, writes code, or generates test cases, and why those rules are harder to satisfy with generative models than teams might assume.
Prover, together with NEAT, Schneider Electric, and Pilz will demo real railway interoperability at InnoTrans: three vendor platforms, one interlocking design, live at Prover's booth.
