Polyspace Code Prover
Polyspace®Code Prover™is a sound static analysis tool that proves the absence of overflow, divide-by-zero, out-of-bounds array access, and other run-time errors in C and C++ source code. It produces results without requiring program execution, code instrumentation, or test cases.Polyspace Code Proveruses semantic analysis and abstract interpretation based on formal methods to verify software interprocedural, control, and data flow behavior. You can use it to verify handwritten code, generated code, or a combination of the two. Each code statement is color-coded to indicate whether it is free of run-time errors, proven to fail, unreachable, or unproven.
Polyspace Code Proverdisplays range information for variables and function return values, and can prove which variables exceed specified range limits. Code verification results can be used to track quality metrics and check conformance with your software quality objectives.Polyspace Code Provercan be used with the Eclipse™ IDE to verify code on your desktop.
Support for industry standards is available throughIEC Certification Kit(for IEC 61508 and ISO 26262) and做资格工具包(for DO-178).
Get Started
Learn the basics of Polyspace Code Prover
Install Polyspace
Install Polyspace products for analysis on desktop or server
Configure and Run Analysis
Set upPolyspace Code Proveranalysis on desktop or server
Review Analysis Results
ReviewPolyspace Code Proverresults in Polyspace desktop user interface or web browser
Tool Qualification and Certification
QualifyPolyspace Code Proverfor DO and IEC Certification
Troubleshooting in Polyspace Code Prover
Resolve unexpected issues inPolyspace Code Prover