In general, the problem with such verification arises because the application is very big, which causes a scaling problem. The application is so large that it makes the verification process very complex. Hence, the verification is taking a long time, more precisely more than 24 hours.
For such huge applications the first recommendation would be to use the Bug Finder instead. Because Bug Finder does not try to prove things, its job is easier and so it can work with huge applications. And even if you plan to use the Code Prover, we recommend to use the Bug Finder before as it will help you to identify run-time errors that would be detected later by the Code Prover: Since it’s better not to have run-time errors in the code to have all of this code being verified, it is more convenient to find them earlier with the Bug Finder. Fixing the run-time errors earlier will actually save you time.
If you want to keep using the Code Prover, then we would recommend to split the verification into several parts: Less code for one verification means less complexity and therefore less scaling problems.
An additional suggestion with the Code Prover would be to use scaling options, i.e. options that reduce the complexity and should help to bypass scaling problems. These options are:
• “Optimize large static initializers” (-no-fold )
• If you use tasks: “Reduce task complexity” (-lightweight-thread-model)
• “Depth of verification inside structures” (-k-limiting). Use the value 2.
• “Precision level” (-O). Use the value 0.
It can be considered as a scaling behavior with Polyspace Code Prover. Would you please also read document attached to MATLAB Answer: What to do when facing a scaling behavior with Polyspace Code Prover? - MATLAB Answers - MATLAB Central (mathworks.com)
