Formal Verification Performance Jump

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!