MathWorks Introduces New Polyspace Code Verification Products

MathWorks today expanded its Polyspace product family with the introduction of two new code verification tools: Polyspace Code Prover and Polyspace Bug Finder. Available with the company’s Release 2013b also announced today, these products deliver an end-to-end software verification capability for early stage development use, spanning bug-finding, coding rules checking, and proof of the absence of run-time errors. This capability ensures the robustness of embedded software that must operate at the highest levels of quality and safety.

Polyspace Code Prover is a formal methods-based verification tool which proves code correctness. Engineers responsible for the safety and certification of their code can use Polyspace Code Prover to provably determine where run-time errors will or will not occur. Color-coded, proof-based results simplify verification tasks, resulting in an efficient and high-quality software development process. In addition, Polyspace Code Prover takes advantage of the MATLAB platform giving users access to powerful MATLAB features such as robust job distribution to computer clusters, scripting for automation, visualization of results, and report generation for certification. Polyspace Code Prover incorporates the functionality previously available in the Polyspace Client for C/C++ and the Polyspace Server for C/C++.

Polyspace Bug Finder identifies run-time errors, data flow problems, and other defects in embedded software. Using static analysis, Polyspace Bug Finder analyzes software control, data flow, and interprocedural behavior.  It can find a variety of defects such as numerical, memory, and other programming errors. Unlike traditional manual review, Polyspace Bug Finder enables engineers to identify, triage and fix code defects quickly for a streamlined development process. The tool also checks compliance to code rule standards such as MISRA and JSF++, custom rules, and produces code quality and complexity metrics. As with Polyspace Code Prover, Polyspace Bug Finder takes advantage of the MATLAB platform for job distribution, scripting, and visualization of results. Both products are integrated with Simulink for use with automatically generated code.

“In providing a comprehensive code verification solution, the Polyspace product family enables engineers to be more confident in the quality and safety of embedded software throughout the development process,” said Paul Barnard, marketing director, Design Automation, MathWorks. “Polyspace Bug Finder and Polyspace Code Prover combine static analysis and formal methods code verification techniques to help engineers find bugs early in the development process and to prove that critical aspects of their software are safe and ready for deployment.”

Polyspace Code Prover and Polyspace Bug Finder are available immediately.