Polyspace Code Prover is a sound static analysis tool that proves the absence of overflow, divide-by-zero, out-of-bounds array access, and certain other run-time errors in C and C++ source code. It produces results without requiring program execution, code instrumentation, or test cases. Polyspace Code Prover uses semantic analysis and abstract interpretation based on formal methods to verify software interprocedural, control, and data flow behavior. You can use it on handwritten code, generated code, or a combination of the two. Each operation is color-coded to indicate whether it is free of run-time errors, proven to fail, unreachable, or unproven.
| Type | Title | Date | |
|---|---|---|---|
| Category | Application Security Tools | Jul 30, 2025 | Download |
| Product | Reviews, tips, and advice from real users | Jul 30, 2025 | Download |
| Comparison | Polyspace Code Prover vs SonarQube Server (formerly SonarQube) | Jul 30, 2025 | Download |
| Comparison | Polyspace Code Prover vs Veracode | Jul 30, 2025 | Download |
| Comparison | Polyspace Code Prover vs Checkmarx One | Jul 30, 2025 | Download |
| Title | Rating | Mindshare | Recommending | |
|---|---|---|---|---|
| SonarQube Server (formerly SonarQube) | 4.0 | 22.8% | 81% | 116 interviewsAdd to research |
| GitLab | 4.2 | 2.7% | 97% | 85 interviewsAdd to research |
Alenia Aermacchi, CSEE Transport, Delphi Diesel Systems, EADS, Institute for Radiological Protection and Nuclear Safety, Korean Air, KOSTAL, Miracor, NASA Ames Research Center
We use this solution to develop software components flashed on ECUs for electronic control units.
Polyspace Code Prover has made me realize it differs from other static code analysis tools because it runs the code. So it's quite distinct in that aspect. We primarily use it in the automotive industry, where we develop components that need to meet certain safety standards.
Polyspace Code Prover helps us minimize the risk associated with these components by identifying potential problems in the code, such as invalid pointer accesses or divisions by zero. These are issues that could be missed during regular code reviews or unit testing, which focus on individual parts and specific input combinations. By leveraging Polyspace Code Prover, we aim to minimize risks as much as possible when developing safe components.
One of the main disadvantages is the time it takes to initiate the first run. Usually, there are a lot of errors initially, and you need to remove dependencies, such as compounded dependencies, to have an initial run. When we compared different tools, we found that the only drawback of Polyspace is the lead time required to have an output.
There's something that can bypass the red errors. This is because you cannot base the policy solely on the presence of a red line or error. Sometimes, this mocks other errors from being reported.
I have been a customer of Polyspace Code Prover for six years. We have the latest version.
The solution is stable.
The solution is scalable. We are a medium enterprise.
There is a lot of help available online that you should consider before talking to someone. However, sometimes it's not about the support; it's about having a case-by-case issue that is harder to solve. In such cases, you need the support team to be involved in your specific use case and provide the necessary help. There are many dependencies on the compiler and other factors. Therefore, each use case will have its own set of problems.
Positive
We use Klocwork, but it is not a substitute for public space. Klocwork offers different functionalities compared to what we need. They have a solution called Bug Finder, which is similar to Klocwork. We are using Klocwork instead of Bug Finder. As for the code approver, there isn't a similar product on the market. We use Clockwork for all our software components except for the safety-critical ones. For the components that require the highest quality, we utilize Polyspace Code Prover instead of Klocwork. This decision is made based on our priority for safety. So, we use Polyspace Code Prover for safety-critical components and Klocwork for all other components.
The initial setup is not so difficult.
The installation takes a couple of hours or less than an hour or two. But it's like cutting up our software, the whole software. It shouldn't take days—maybe seven to eight days—to have an initial run with no errors and all the dependencies removed.
Two engineers are assigned per project for this activity, and they work on it throughout the entire project. They are not typically responsible for the entire component. The benefit of their involvement is that they can assist the developers at the front end of the component, but they are not involved in developing all of the components. Generally, we assign this task to two engineers who receive the report and deliver it to the other developers.
We are required to maintain it. We have to rerun it every time there is a code change.
Two persons are required per project for maintenance. However, in our organization, we have a large volume of projects. Therefore, it requires a significant number of people. We have multiple sites and around 50 projects. We enforce policies, ensure their strength, and provide maintenance.
The solution is not really cheap, but it wouldn't cost too much either. It is something you need. Its benefits outweigh its cost. It has a good price point. It has a yearly license fee.
I advise you to check what exactly you need out of this tool. Sometimes, you might not need something as complex as a code prover. However, in a use case where you want to check all possible combinations and inputs to ensure that the software does not behave incorrectly, you will definitely need to use Polyspace Code Prover. It is not humanly possible to perform these checks manually. If you are delivering a product with a quality rating or if it will impact people's lives in some way, then Polyspace Code Prover is essential.
But if your application is not that critical, if it does not significantly impact people's lives, and if you can afford not to use it, then you can definitely go without it. Polyspace Code Prover finds many problems that are missed during normal unit testing. However, if you cannot afford the cost, you must evaluate the importance of quality.
Overall, I rate it an eight out of ten because of the time it takes.
