Performance issues with formal verification

We’ve all been there, waiting for the theorem prover to answer. Getting up for a cup of coffee, bugging a colleague… still no answer. This can be standard behaviour when doing formal verification. The requirements are difficult to prove, the system manages to escape into some dark corner not easily approached by the theorem prover. If things are really bad, then the waiting might continue for hours, days, even weeks!

More is not better

The common remedy for this condition is to get more computers, more powerful computers, more memory, parallel computers, more, more… more usually helps to solve the current situation. But soon another larger system comes along and the condition returns. What I am saying is that, usually, perfomance issues when doing formal verification are a symptom of a more serious disease. And trying to cure it with more computer power is like treating cancer with stronger painkillers; it only addresses the symptom, not the cause.

System disharmony

In my experience, the cause of performance issues when doing formal verification is not lack of computer power. It is rather an indication that the requirements and the system verified are not in harmony. With this, I mean that the system might satisfy the requirements, but not in an obvious way. If the requirements are satisfied, then they are done so in some roundabout, tricky way, not by some straightforward checks, making them hard to prove.

The root cause of this disharmony is usually that the system was not developed for verification, causing the fulfillment of the requirements to be addressed late in the development process. The obvious cure is prophylax. Ideally, the requirements should be available at the beginning of the development of the system. Then the developers can design the system so that it satisfies the requirements in an obvious way. This will make the requirements easy to prove and all performance issues go away. Furthermore, formal verification should be introduced as early as possible in the process so the developers have a chance to confirm that they are on the right track.

In case you are wondering, this is how development is done in the Prover Trident process.