Prover Certifier performance jump with IC3

Prover Certifier now has a very powerful IC3 strategy, thanks to the release of Prover PSL 5.4. Prover PSL is used in Prover Certifier, our formal verification-based product for automatic production of safety evidence for safety-critical applications.

If you are interested in Formal Verification, then you have probably heard of IC3, also known as PDR. Simply put, IC3 is a way for model checkers to automatically create lemmas that make proofs inductive: the generated lemmas will be added to the proof obligations and induction can then be used to prove the proof obligations in conjunction with the lemmas.

When IC3 was presented, it was considered to be a very interesting step forward. Lemma-generating strategies had existed before—for example, interpolation—but IC3 introduced a more sophisticated way to generate lemmas. In comparison, IC3 seemed able to solve more problems than interpolation.

We implemented IC3 a couple of years ago, but when we compared that implementation with interpolation, we were a bit disappointed. We had been optimizing our implementation of interpolation over many years, and it had become hard to beat. We obviously had more work to do with IC3. Now, after much work, we are happy to release Prover PSL 5.4, which includes dramatic performance improvements for IC3.

Dramatic performance improvements for IC3

With the Prover PSL 5.4 release, IC3 is now usually faster than interpolation. We also see examples where IC3 succeeds in proving properties that were previously only possible to analyze with bounded model checking. One of our customers had a property that they were not able to prove, but they had analyzed it to depth 50 using BMC, which took almost a day. With our new IC3 implementation, the property could be proved in five and a half minutes.

There are still some cases when interpolation wins. We have tried to spot the patterns, but so far, we have not been able to. If you have some rules of thumb regarding when to expect interpolation to be better than IC3 or vice versa, we would be very interested to hear about them.

An example command line you can try:

psl –hll myhardmodel.hll -analyse all join in 1 group –solver 3 -ic3

Tips:

• IC3 works best without preprocessing, so Solver 3 is preferred to Solver 1+3.
• Analyzing all proof obligations together is usually beneficial with IC3.
• As usual you can combine with other strategies. For example, try induction first, then IC3, and finish with interpolation.

Using IC3 to produce formal verification-based safety evidence

Prover Certifier has been certified by TÜV Nord as compliant with CENELEC EN 50128 up to SIL4. Prover Certifier uses Prover PSL to produce a proof with a proof log, but also provides an independent proof checker that will double-check the proof log. The proof log from IC3 is very small compared to one produced by interpolation. In some cases we tried, interpolation produced logs that were more than a thousand times bigger than the ones from IC3. Small proof logs make IC3 usable in practice in many cases where interpolation produces logs that are too big.

We’re looking forward to hearing your success stories about IC3!