
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!

How safe and efficient are your rail control systems? Let’s find out!
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.