MathWorks 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, the new products provide a software verification capability for early stage development use, spanning bug-finding, coding rules checking, and proof of the absence of run-time errors.
Polyspace Code Prover is a formal methods-based verification tool that proves code correctness. Engineers responsible for the safety and certification of their code can use it to provably determine where run-time errors will or will not occur. In addition, Polyspace Code Prover takes advantage of the MATLAB platform, giving users access to MATLAB features such as job distribution to computer clusters, scripting for automation, visualization of results, and report generation for certification.
Polyspace Bug Finder identifies run-time errors, data flow problems, and other defects in embedded software. Using static analysis, it analyzes software control, data flow, and interprocedural behavior. It can find a variety of defects such as numerical, memory, and other programming errors. The tool also checks compliance to code rule standards such as MISRA and JSF++, custom rules, and produces code quality and complexity metrics.
“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.”
For more information, visit MathWorks.
Sources: Press materials received from the company and additional information gleaned from the company’s website.