Share your experience using Polyspace Code Prover

We use it for all projects where we write our own code. So, it could be vertical control, cluster infotainment, or competitor systems; we use it everywhere.

We use it for smaller models and for Simulink models. However, it crashes when we have too many files/functions. When we use Code Prover on large applications, it sometimes crashes.

I work with Simulink models, where Prover is fully integrated.

Prover enhanced our code verification process. That's why we use this type of tool. We need a static code analysis tool. 

When we work on safety modules, it is mandatory to fulfill ISO 26262 compliance. Using Prover helps fulfill the standard on top of many other quality checks, like division by zero, data type casts, and null pointer dereferences. So, we have numerous checks that improve our code.

We leverage many features that are effective for identifying bugs because they all complement each other. Just using one wouldn't be enough for quality purposes. We need the whole set.

There are two main areas of improvement. 

1. False negatives and false positives. 
2. The speed of the validation itself.

Another area I see for improvement is scalability, particularly when dealing with large software systems. While Polyspace is effective for individual components and smaller applications, its performance can be impacted when analyzing entire systems all at once.

There are limitations with handling large-scale applications.

I started using Code Prover recently since it became integrated into MATLAB just six months ago in my company. It works well.

We need to compare it to similar tools Fortify, Checkmarx, etc.

They often detect more quality issues, especially related to code flow, and they're generally faster. 

However, there is a trade-off in these tools: speed versus quality. It's not ideal to sacrifice one for the other entirely. But, some other tools have a better balance.  

While finding bugs is good, it's hard to quantify the exact impact. 

We understand it's more expensive, but we lack concrete data to prove using it definitively gives us a clear benefit.

We use the paid version. 

If you're using Simulink and Stateflow models within MATLAB, integrating with Polyspace Code Prover is very convenient because they're fully supported. There's a link between the code in the Simulink blockset, which makes verification efficient and practical.

Overall, I would rate the solution a six out of ten. It is not a bad tool, it is just not the best tool. 

We use the solution to check the runtime issues of our programming.

The product runs the code based on our application loop and tries to find run time overflows of the variable and out-of-boundary memory issues. The product detects memory corruptions. It also detects undefined memory access and memory dereference. These are value-adding features.

The run time analysis process must be improved. If we do not run with the main loop, it generates its own main and doesn’t allow developers to modify the execution sequences. The solution must provide more flexibility to the developers to manipulate the runtime analysis tools. The developer must be allowed to modify the main sequence. It will be very easy for them to test their use cases. Otherwise, Polyspace generates a random main file and executes all the functions randomly.

I have been using the solution for four months.

The tool has some stability issues. It is 90% stable. It provides false positive reports sometimes. It must be stabilized.

The product is scalable. We have 20 people in our team.

The support provides good suggestions and resolves our issues.

Positive

I have used Coverity. It only does the static analysis of the code. I have also used Helix QAC. Polyspace gives more reliable information compared to Coverity and Helix QAC.

The installation is easy, but the people working on it must be trained.

We deployed the tool in-house.

I recommend the product to others. Overall, I rate the tool an eight out of ten.