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
Do you have experience in leading strategic and complex customer projects? Are you looking for an opportunity to leverage your experience throughout our company? Then this role might be right for you! We are now recruiting to a new position as a Commercial Project Management (PM) Lead.
Prover uses formal methods to make railway signaling provably safe. Our solutions build safe, reliable, and cost-efficient systems that move and protect millions of passengers every day. Through our Open Signaling Initiative, we're reshaping how the industry builds and maintains signaling systems across Europe and beyond. Now we're looking for someone to join us and bring AI, LLMs, and agentic workflows into the heart of how we work and what we build.
Meet Prover at RailTech Europe in Utrecht, March 4–5. Visit Booth 2.509 and join our workshop on migration of signaling systems to PLC-based SIL 4 solutions.
