
We are starting to receive customer feedback about our model checker PSL. Truly exciting reading!
“Our proof time has decreased by 12 times on average”
one customer said. The comparison was made with the old model checker Tecla. Another customer reported:
“7 times faster on average”
and when they tried our new feature Turbo-threading that utilizes parallel computing, they came back with
“60-140 times faster!”
I actually anticipated positive feedback since our own tests had shown big improvements; one problem that used to take 83 days without Turbo-threading took only two days when we enabled Turbo-threading. But to get enthusiastic feedback from customers is really rewarding.
PSL – The story
The story of PSL began in 2015 when we took the decision to implement an entirely new model checker from scratch. Throwing out a working product and starting over from scratch is known as “the Netscape mistake”, since Netscape did exactly that – and died. But we took the brave decision to do it, because we saw that making Tecla considerably faster by simple refactoring would be very difficult.
The first step was to reach a state where the new product would be as good as the old one. At that point we could abandon Tecla by offering our customers to convert when necessary. The next step was to add new features and to fine-tune existing ones. Now the fun started. We could watch how the product improved for each addition. Well-known academic strategies such as IC3/PDR entered, but we also made surprising improvements to the old interpolation strategy, making it better than IC3/PDR in many cases. Proof logging was made much more efficient, and incremental SAT was added to aid searches for deep counterexamples. With the recent introduction of Turbo-threading we have been able to develop a model checker that is much better than anything we have seen before.
These big improvements have inspired us to take the next performance jump. Being the fastest is not enough when you compete with yourself! And as we know that our customers systems become more and more complex, performance is key!
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 is partnering with Eiffage Énergie Systèmes on the Villeneuve Demain project, delivering railway signaling software for the PAVS system at SIL4 safety level.
Using Prover’s automation tools, the solution ensures EN 50716 compliance, facilitates future maintenance, and enables reuse across similar systems.
Prover will be at Train & Rail, meet us in our booth located at A06:31.
Learn how Prover’s Relay Signaling Migration enables safe, efficient modernization of legacy railway systems with formal verification and digital twin technology.