Fact-checked by Grok 2 weeks ago

Polyspace

Polyspace is a suite of static code analysis tools developed by MathWorks for verifying the absence of runtime errors, detecting vulnerabilities, and ensuring compliance with coding standards in C, C++, and Ada source code. It employs formal methods, particularly abstract interpretation, to exhaustively analyze code semantics without executing the program, proving that certain classes of defects—such as buffer overflows, division by zero, or integer overflows—either exist or are impossible. Originally developed by the French company PolySpace Technologies, which was founded in 1999 in Grenoble as a spin-off from INRIA research in software verification, the technology was acquired by MathWorks in April 2007 to enhance its embedded software development offerings. The Polyspace product family includes specialized components like Polyspace Bug Finder, which identifies runtime errors, concurrency issues, and security vulnerabilities in generated or hand-written code, and Polyspace Code Prover, which formally verifies the correctness of critical code statements against safety and security standards such as for , for automotive systems, and for industrial applications. These tools integrate seamlessly with development environments like /, continuous integration pipelines, and issue-tracking systems such as , enabling teams to automate code quality checks throughout the software lifecycle. Widely adopted in safety-critical industries including , automotive, medical devices, and semiconductors, Polyspace reduces testing efforts by providing proof-level assurance and remediation guidance, thereby minimizing risks in embedded systems where reliability is paramount.

Overview

Definition and Purpose

Polyspace is a suite of static code analysis tools developed by for verifying the source code of programs written in C, C++, and Ada. It performs to either detect runtime errors or mathematically prove their absence in the analyzed code. The core purpose of Polyspace is to enhance and reliability, particularly in safety-critical systems, by identifying potential defects such as buffer overflows, arithmetic overflows, null pointer dereferences, and without requiring code execution. This approach enables developers to address issues early in the development process, reducing the risk of failures in deployed software where consequences could be severe. In contrast to dynamic testing methods, which execute the code with selected inputs to sample possible behaviors, Polyspace employs to exhaustively examine all feasible execution paths and states, offering comprehensive coverage rather than probabilistic sampling. This exhaustive nature makes it especially suitable for verifying complex codebases where incomplete testing could overlook critical errors. The underlying technique used by Polyspace was developed in the , and the tools were created to meet the stringent reliability demands of embedded systems, where resource constraints and real-time requirements amplify the impact of software defects. It leverages as the foundational technique for this .

Key Products

Polyspace offers a suite of specialized tools designed to enhance in critical systems, primarily through static and dynamic analysis of C, C++, and Ada code. Since MATLAB R2024b, these products can be run from the unified Polyspace Platform user interface, which supports both desktop and server workflows for improved integration. The main products include Polyspace Bug Finder, Polyspace Code Prover, Polyspace Test, and Polyspace Access, each targeting distinct aspects of code verification, testing, and review while supporting integration into development workflows. Polyspace Bug Finder focuses on static analysis to detect runtime bugs, enforce coding rules, and identify security vulnerabilities in C and C++ code. It performs checks against standards such as , C++14, and CERT C/C++, simulating potential runtime errors like buffer overflows and concurrency issues without executing the code. Additionally, it generates code metrics, including , to assess and improve code maintainability. Polyspace Code Prover employs based on to exhaustively prove the absence of runtime errors in critical code sections, analyzing all possible execution paths. Results are presented via color-coding: for statements proven safe, for those containing definite errors, and for unproven assumptions requiring further review. This approach ensures functional correctness and supports compliance with safety standards like ISO 26262. Introduced in MATLAB R2023b, Polyspace Test enables dynamic unit and for embedded C and C++ systems, including automated generation to target boundary conditions and gaps. It supports test execution on host machines or hardware targets, using an xUnit-based API or graphical interface, and measures coverage metrics such as decision, condition, and (MC/DC). Polyspace Access enables software teams to review static results, track defects and metrics, and collaborate on improvements throughout the lifecycle. It integrates with issue-tracking systems like and supports on-premises or cloud deployment for centralized monitoring. These products complement each other in a typical : Polyspace Bug Finder conducts initial scans to identify and prioritize defects early in , Polyspace Code Prover provides for high-assurance components, Polyspace Test validates the through dynamic execution and coverage , and Polyspace Access facilitates result review and team collaboration. This integration allows seamless transitions from static detection to proof, testing, and monitoring, often within IDEs or continuous integration pipelines.

Technical Principles

Abstract Interpretation

Abstract interpretation is a formal method for approximating the semantics of programs to statically analyze properties such as safety and correctness without executing the code. Developed as a mathematical , it enables the construction of program analyses by defining approximations of the program's behavior that are computable and decidable. At its core, distinguishes between concrete semantics, which precisely describe all possible execution traces and states of a program, and abstract semantics, which provide a sound over-approximation of these behaviors to ensure decidability for infinite or complex state spaces. The concrete semantics capture the exact, potentially infinite set of program outcomes, but direct computation is often infeasible due to undecidability. In contrast, the abstract semantics map program states to elements in a chosen abstract domain, allowing finite representations and iterative computations that conservatively include all possible concrete behaviors. Abstract domains, such as intervals for numerical values, define the structure for these approximations; for example, the interval domain represents variable ranges like [0, 100] to bound possible values without enumerating each one. In Polyspace, applies over-approximation to symbolically explore all feasible execution paths, enabling the verification of properties like the absence of errors across the entire program. By propagating abstract values through and , it models the effects of operations on approximated states, proving that no erroneous behavior is reachable if the abstract analysis shows none. This technique ensures : any property proved to hold in the abstract semantics definitively holds in the concrete semantics, with no false negatives for verified absences. Additionally, its scalability stems from the use of efficient abstract operators and domains tailored to large-scale code, avoiding the exponential costs of exhaustive path enumeration. A representative example is the use of interval abstraction to detect potential integer overflows in loops. Consider a loop that repeatedly increments an variable starting from an initial value; the interval domain computes the widening bounds of the variable's possible range at each iteration, determining if it exceeds the maximum representable value under any input conditions. If the analysis shows the range stays within safe limits, overflow is proved absent; otherwise, it flags potential issues for further scrutiny.

Verification Techniques

Polyspace employs over abstract domains to compute an over-approximation of the reachable program states, enabling the verification of code against potential run-time errors without executing the program. This process begins with an initial abstract state representing possible inputs and iteratively applies abstract transformers for each statement, propagating states through the until a fixed point is reached where further iterations yield no changes. The abstract domains used include for numerical values, octagons for linear relations, and specialized domains for memory modeling, ensuring scalability for large codebases while maintaining soundness through conservative approximations that include all possible concrete behaviors. To handle pointers and arrays, Polyspace integrates field-sensitive value analysis within its abstract domains, tracking possible and memory locations to detect issues such as buffer overflows and invalid accesses. Pointers are modeled as offsets within allocated regions, with abstract tracking of possible targets to avoid under-approximations that could miss errors. For arrays, bounds are inferred dynamically from the abstract propagation, verifying index computations against allocation sizes. Concurrency is addressed through semantic analysis that constructs an abstract model of task interactions, identifying data races on shared variables by over-approximating possible interleavings and access patterns without enumerating all schedules. In terms of , Polyspace performs a model checking-like exploration of the abstract state space to prove temporal properties such as the absence of run-time errors along all feasible paths. This forward reachability analysis simulates execution traces in the abstract domain, confirming that no state leads to an erroneous condition like or . While primarily forward-oriented, the technique leverages the fixed-point semantics to establish inductive invariants over program points, akin to proving safety properties in but scaled via rather than explicit state explosion. The verification results are presented through a color-coded scheme directly in the source code: indicates operations proven safe on all paths, denotes proven errors on some paths, and marks unproven where the assumes environmental conditions or user-provided assertions to resolve ambiguity. Justification files accompany these outputs, documenting assumptions and proofs for purposes, such as generating reports that detail the abstract traces supporting results or rationales for justifying ones. Undecidability in verification, arising from features like unbounded loops or recursion, is managed through conservative over-approximations that guarantee no false negatives, ensuring that any overlooked error is not falsely deemed safe. Users can introduce domain-specific assumptions, such as loop bounds or pointer invariants, to refine the abstract model and reduce orange results without compromising soundness. This approach prioritizes exhaustive coverage over precision, allowing iterative refinement. Unlike , which exhaustively enumerates concrete states and can suffer from state-space explosion, Polyspace's emphasizes scalable over-approximation, computing a finite fixed point that bounds the possible behaviors and enables of industrial-scale code without timeout or memory issues. This ensures termination and but may introduce false alarms (orange checks) resolvable by user intervention, contrasting model checking's potential for exactness at the cost of completeness in complex systems.

History

Origins and Acquisition

Polyspace technology originated in the late as a product of PolySpace Technologies, a company founded in 1999 by Alain Deutsch and Daniel Pilaud in , . The company emerged as a spin-off from research conducted at INRIA (Institut National de Recherche en Informatique et en Automatique), building on foundational work in for analyzing safety-critical software. This academic heritage positioned PolySpace Technologies to develop innovative tools for static code verification, addressing the growing need for reliable embedded systems in high-stakes environments. From its inception, PolySpace Technologies concentrated on creating verification tools tailored for and automotive applications, leveraging to ensure error-free operation in systems. These tools automatically detected errors at , targeting industries where software reliability was paramount, such as and automotive sectors, to mitigate risks in safety-critical codebases. The emphasis on techniques allowed early adopters to prove the absence of common programming errors, enhancing confidence in complex, resource-constrained systems. On April 25, 2007, acquired PolySpace Technologies to incorporate its verification capabilities into the and ecosystems, facilitating seamless integration for developers. Following the acquisition, the technology underwent rebranding as Polyspace, aligning it with ' product suite and enabling enhanced workflows for code generation and analysis. An initial post-acquisition release, Polyspace 6.0, arrived in October 2008 as part of R2008b, marking the first unified offering under and expanding accessibility for verifying hand-written and model-generated code.

Post-Acquisition Developments

Following its acquisition by MathWorks in 2007, Polyspace was incorporated into the MATLAB and Simulink environments to enhance model-based design verification workflows, with initial integrations enabling static analysis of generated code and handwritten components starting in releases shortly thereafter. Major releases have progressively expanded Polyspace's capabilities. The R2010b update improved support for advanced programming constructs in code verification, allowing more comprehensive analysis of complex embedded software. In R2020a, Polyspace Bug Finder achieved full compliance checking for all CERT C rules, including detections for hardcoded sensitive data and thread-safety issues, while extending analysis to all C/C++ code forms imported into Simulink, such as those from C Function blocks and Stateflow charts. The R2023b release introduced Polyspace Test, a dedicated product for dynamic testing that supports developing, managing, and executing unit and integration tests for C and C++ embedded code. Post-acquisition expansions have broadened Polyspace's language and domain coverage. Support for Ada code verification was maintained and enhanced through specialized tools like Polyspace Client for Ada and Polyspace Server for Ada, which prove the absence of runtime errors in Ada83 and Ada95 applications. Cybersecurity features were added to detect vulnerabilities in C/C++ code, with alignment to standards including ISO/SAE 21434 for automotive cybersecurity risk management by 2024. Additionally, cloud-based analysis options were implemented, enabling Polyspace to run on cloud platforms and integrate seamlessly into continuous integration/continuous delivery (CI/CD) pipelines for scalable verification.

Capabilities

Bug Detection and Analysis

Polyspace Bug Finder employs static analysis to detect a wide range of runtime errors in C and C++ code, including memory leaks (such as failure to release allocated memory after use, corresponding to CWE-401), uninitialized variables (CWE-457), and buffer overflows (CWE-119). It also identifies security vulnerabilities, such as hard-coded credentials (CWE-798) and cleartext transmission of sensitive information (CWE-319), among over 100 CWE categories mapped to its defect checkers. This comprehensive scope covers hundreds of potential defects without requiring code execution, focusing on control flow, data flow, and interprocedural behaviors to simulate possible execution paths and uncover issues like division by zero or array bounds violations. The tool provides analysis features such as traceability matrices to link code elements back to originating models in or Stateflow, enabling developers to trace defects to their design sources. It simulates execution paths through of control and data flows, estimating the number of static paths and highlighting branches. Additionally, Polyspace computes complexity metrics, including (measuring linearly independent paths in functions) and function stress complexity (assessing internal structure and external connections), to quantify code maintainability and identify overly complex sections. For rule checking, Polyspace Bug Finder enforces coding standards like :2012, supporting 141 of the 149 decidable rules with options for customizable rule sets via annotations or configuration files. Users can prioritize violations based on severity, impact, or custom criteria during review, allowing focus on high-risk issues such as those violating essential MISRA directives for safety-critical systems. Analysis outputs include detailed reports with visualizations like call graphs, event traces, and debugger-like views that suggest fixes, such as inserting initialization statements for uninitialized variables. False positives are filtered through user annotations and automated checks against quality thresholds, reducing review time. Historical compares current results with prior runs, tracking defect resolution and code quality improvements over iterations.

Code Proving and Certification

Polyspace Code Prover performs an exhaustive static analysis of C and C++ source code, evaluating all possible execution paths and input values without running the program, to generate proof objectives for each statement that demonstrate the absence of critical run-time errors such as overflows, divide-by-zero, and out-of-bounds accesses. This process aligns with objectives, including those for model-based development (MB.A-5, objectives 2-4 and 6) and (FM.A-5, objectives 2-4, 6, and 10-13), enabling justification for eliminating or reducing certain verification activities under Tool Qualification Level-4 (TQL-4) for Design Assurance Level A (DAL A) certification. The tool produces certification artifacts essential for , including justification files that document proof results and rationale for error absence, structural coverage reports for source and (MB.A-7, objectives 1 and 4-7), and matrices linking code elements to low-level requirements (MB.A-5, objectives 1-3, 5, and 6). These outputs, certified by SÜD for and and supporting DO-178C qualification with verifiable artifacts, facilitate audits by providing evidence of code robustness. To address incomplete models, such as external libraries or hardware interfaces, Polyspace supports user-defined axioms that specify behavioral assumptions for unanalyzed components, ensuring proofs remain valid while highlighting dependencies for manual review. Proof validation involves checking these assumptions through to confirm their consistency with the overall verification goals. For scalability, Polyspace handles large codebases exceeding millions of lines of code by leveraging across multiple cores and integration with pipelines via Polyspace Code Prover Server, minimizing analysis time for enterprise-scale projects.

Testing and Integration

Polyspace Test enables dynamic testing through automated unit test generation, execution, and coverage analysis for C and C++ code in systems. It automatically generates test cases to achieve coverage objectives and value testing, supporting the of stubs and mocks via an xUnit-compatible or graphical interface. Test execution occurs on host computers or target hardware, with built-in profiling for memory usage and performance metrics. Coverage metrics include decision, condition, and modified condition/decision (MC/DC) analysis to assess test completeness. Integration options extend Polyspace's dynamic testing into development environments, including IDEs such as , , and via plugins or as-you-code extensions. For CI/CD pipelines, it connects with tools like Jenkins and GitHub Actions to automate test runs and reporting. Issue tracking integration with allows direct creation and linking of tickets from analysis results through Polyspace Access. The end-to-end workflow begins with code import from repositories or models, proceeds through test generation and execution, and concludes with exportable reports detailing coverage and defects. This process supports co-simulation with for verifying generated code alongside model behavior. support includes automated analysis triggered from repositories, with an enabling custom scripts for tailored workflows.

Applications

Industry Sectors

Polyspace finds extensive application in safety-critical industries where must demonstrate high reliability to prevent failures that could endanger lives or missions. Its abstract interpretation-based analysis enables exhaustive of for errors, supporting with sector-specific standards and reducing the need for extensive testing. In the and sector, Polyspace is employed to verify flight software and control systems in , satellites, helicopters, and defense platforms, ensuring dependability for mission-critical operations. It facilitates by proving the absence of errors like overflows and divide-by-zero, which helps lower certification costs and efforts associated with airborne systems. The leverages Polyspace for in advanced driver-assistance systems (ADAS), electronic control units (ECUs), and software, including adherence to architectures. It supports requirements up to ASIL D by providing formal proofs of code correctness, enabling suppliers to deliver verified components across the supply chain. A notable example is , which integrates Polyspace into its software factory workflow to detect and resolve runtime errors prior to code integration, accelerating development while maintaining ISO 26262-compliant quality. For medical devices, Polyspace addresses in embedded diagnostics and therapy delivery systems, such as infusion pumps, implanted devices, and robotic surgical platforms, targeting classes up to III for life-sustaining applications. Its static analysis confirms software quality by verifying absence of defects that could lead to hazardous failures, streamlining documentation for regulatory audits. In semiconductors and communication, along with other embedded systems domains, Polyspace verifies firmware and drivers for chip design and network equipment, enhancing robustness against vulnerabilities in high-volume production environments. It minimizes the attack surface in business-critical systems by proving error-free behavior across diverse hardware configurations.

Compliance and Standards

Polyspace supports key safety standards essential for high-integrity software development in critical domains. For avionics, it aligns with DO-178C by providing verification artifacts and reports that facilitate certification processes up to Level A objectives. In the automotive sector, Polyspace is certified by TÜV SÜD as a qualified tool for ISO 26262 compliance, enabling ASIL D verification through static analysis and proof of absence of runtime errors. For general functional safety, it meets IEC 61508 requirements, with TÜV SÜD certification supporting SIL 3 levels via comprehensive code verification. Additionally, Polyspace aids compliance with IEC 62304 for medical device software, generating evidence for Class III devices through static analysis integrated with Model-Based Design workflows. The tool enforces a range of coding rules to promote reliable and maintainable code. Polyspace checks all versions of and C++, including the latest MISRA C++:2023 guidelines targeting , to detect deviations that could lead to . It also verifies CERT C and CERT C++ secure coding standards, focusing on vulnerabilities like buffer overflows and resource leaks. For automotive applications, support extends to C++14 rules, which build on MISRA to ensure safety in embedded systems. Furthermore, Polyspace implements JSF++ (Joint Strike Fighter Air Vehicle C++ coding standards), enforcing over 200 rules for defense and projects to minimize risks in complex software. Polyspace addresses security standards to mitigate threats in connected systems. It maps defects to (CWE) identifiers, allowing users to filter and prioritize issues based on the CWE database for comprehensive vulnerability coverage. Following the 2021 publication of ISO/ 21434, Polyspace incorporated support for this cybersecurity standard, enabling verification of road vehicle software against threats through static analysis and artifact generation. Compliance reporting in Polyspace automates the production of audit-ready evidence, streamlining certification efforts. It generates detailed reports on code verification results, including proof of runtime error absence and rule compliance checks performed by Polyspace Bug Finder. Traceability is achieved by linking analysis results to requirements, facilitating bidirectional mapping for standards like and ISO 26262. Coverage metrics, such as statement, decision, and MC/DC, are automatically collected and reported to demonstrate testing thoroughness required by safety standards.

References

  1. [1]
    Polyspace - MATLAB & Simulink
    Polyspace provides a unified solution for managing, measuring, and monitoring software quality, making critical code safe and secure throughout the development ...
  2. [2]
    Abstract Interpretation - MATLAB & Simulink - MathWorks
    Learn how to use abstract interpretation to verify software quality with Polyspace products. Resources include videos, examples, and documentation.
  3. [3]
    The Mathworks acquires PolySpace Technologies - EE Times
    Apr 25, 2007 · The Mathworks Inc., developer of technical computing and model-based design software, announced it has acquired PolySpace Technologies, ...Missing: history | Show results with:history
  4. [4]
    PolySpace Technologies - Products, Competitors, Financials ...
    Founded in 1999, PolySpace is the fruit of the INRIA, a French national institute for research in computer science and control, expertise in the field of ...
  5. [5]
    Polyspace Bug Finder - MATLAB - MathWorks
    Polyspace Bug Finder identifies run-time errors, concurrency issues, security vulnerabilities, and other defects in C and C++ embedded software.
  6. [6]
    Polyspace Code Prover - MATLAB - MathWorks
    Polyspace products make critical code safe and secure by testing and monitoring software quality throughout the development lifecycle. Polyspace Access.
  7. [7]
    What Are Polyspace Static Code Analysis Products? - MathWorks
    Sep 20, 2022 · Polyspace static code analysis products enable engineers to develop C, C++, and Ada embedded software that is safe, secure, and compliant ...
  8. [8]
    Static Code Analysis - MATLAB & Simulink - MathWorks
    Static code analysis, or static analysis, is a software verification activity that analyzes source code for quality, reliability, and security without ...
  9. [9]
    Using formal methods for sophisticated static code analysis
    Jun 6, 2012 · In this Product How-To design article, Jay Abraham of Mathworks uses the company's Polyspace code verifier to explain the use formal ...
  10. [10]
    Polyspace Products and Software Development Workflows
    The Polyspace® group of products provide a unified solution for managing, measuring, and monitoring C/C++ code quality throughout a software development ...
  11. [11]
    Code Prover Result and Source Code Colors - MATLAB & Simulink
    Showcasing the icons for red, gray, orange, and green checks in the Results. Run-Time Checks. Polyspace Code Prover checks each operation in your code for ...
  12. [12]
    MathWorks Introduces Simulink Fault Analyzer and Polyspace Test ...
    Sep 21, 2023 · R2023b also includes Polyspace Test™, a new product that empowers engineers to develop, manage, and execute C and C++ code tests in embedded ...
  13. [13]
    Polyspace Test
    ### Summary of Polyspace Test (https://www.mathworks.com/products/polyspace-test.html)
  14. [14]
    [PDF] Abstract interpretation: a unified lattice
    Cousot[76]. They are shown to be consistent with the abstraction process. Practical examples illus- trate the various sections. The conclusion points out ...
  15. [15]
    [PDF] Abstract Domains for Bit-Level Machine Integer and Floating-point ...
    For instance, the interval domain [9] allows inferring vari- able bounds. Bound properties allow expressing the absence of many run-time errors (such as.
  16. [16]
    Polyspace Static Analysis Notes - MATLAB & Simulink - MathWorks
    The Polyspace static analysis solution uses a formal methods technique known as abstract interpretation. This technique bridges the gap between conventional ...
  17. [17]
    [PDF] Static Analysis using Abstract Interpretation
    integer overflow. Harder objectives : assertions (pre/post invariants) ... Memory analysis - Memory abstract domain. Memory abstract domain. Based on ...
  18. [18]
    Concurrency: Race Conditions and Deadlocks - MATLAB & Simulink
    The Polyspace engine can statically detect concurrency issues and trace the control and data flow to help debug the root cause of an issue.Missing: point pointers arrays
  19. [19]
    [PDF] Applications of Abstract Interpretation - Patrick Cousot
    PolySpace.com produces ADA verifier (now other tools available). Other ... Cousot and R. Cousot. An abstract interpretation-based frame- work for ...
  20. [20]
    [PDF] Comparing Model Checking and Static Program Analysis - USENIX
    Static program analysis and model checking are two dif- ferent techniques in bug detection that perform error checking statically, without running the ...<|control11|><|separator|>
  21. [21]
    Polyspace - User Interface Through Bug Fixes or Justifications
    File Exchange ... These reports allow standards committees such as certification authorities to verify if a Polyspace result was justified for approved reasons.
  22. [22]
    https://www.usenix.org/legacy/event/ssv10/tech/full_papers/Vorobyov.pdf
  23. [23]
    [PDF] History of Abstract Interpretation - Math-Unipd
    Aug 12, 1976 · Abstract—We trace the roots of abstract interpretation and its role as a foundational principle to understand and design static program ...
  24. [24]
    [PDF] Annual Report INRIA 1999
    PolySpace Technologies is a company specializing in the development of software testing and validation environments. The company markets first generation ...
  25. [25]
    The MathWorks acquires PolySpace Technologies, developer of ...
    NATICK, Mass., 26 April 2007. The MathWorks has acquired PolySpace Technologies, a software company based in Grenoble, France, that provides embedded softwareMissing: history | Show results with:history
  26. [26]
    PolySpace Technologies - Automatic Run-Time Error Detection
    PolySpace Technologies - Automatic Run-Time Error Detection. ... avionics, aerospace, defence, railways, automotive, energy and telecom fields.
  27. [27]
    MathWorks acquires PolySpace Technologies - 2007-04-25
    MathWorks acquires PolySpace Technologies on 2007-04-25 for an undisclosed amount.
  28. [28]
    Polyspace Verification - YUMPU
    Dec 9, 2012 · March 2008 Online Only Revised for Version 5.1 (Release 2008a)<br />. October 2008 Online Only Revised for Version 6.0 (Release 2008b)<br />.
  29. [29]
    Integrate Polyspace with MATLAB and Simulink - MathWorks
    Integrate Polyspace with MATLAB and Simulink to identify potential bugs, run-time errors, and coding standard violations in your model and code.
  30. [30]
    MathWorks Announces Release 2010b of MATLAB and Simulink ...
    Sep 13, 2010 · With R2010b, Simulink offers a new signal type and subsystem enhancements that the company says help reduce block counts, simulation time, and ...
  31. [31]
    What's New in Polyspace R2020a? - MATLAB & Simulink - MathWorks
    Release 2020a of the Polyspace® products complete many existing workflows and introduce some new capabilities. Polyspace Bug Finder™ now supports all CERT C ...
  32. [32]
    Polyspace Client for Ada - MATLAB - MathWorks
    Polyspace static code analysis tools detect and prove the absence of overflow, divide-by-zero, out-of-bounds array access, and other run-time errors in ...Missing: tool definition
  33. [33]
    ISO 21434 Support in MATLAB, Simulink, and Polyspace - MathWorks
    ISO/SAE 21434:2021 is an international standard for the automotive industry, addressing cybersecurity risks within modern road vehicles.
  34. [34]
    Static Code Analysis in the Cloud with Polyspace - MathWorks
    Polyspace products for static code analysis can also be easily integrated with the software development processes and services offered by the cloud providers.
  35. [35]
    CWE Coding Standard Coverage Using Polyspace - MathWorks
    This table lists CWE categories that you can map to Polyspace defect checkers and Polyspace CWE coding rule checkers. CWE categories are groupings of weaknesses ...
  36. [36]
    Systems and methods for analyzing violations of coding rules
    The Polyspace Bug Finder is a static analysis tool that analyzes control flow, data flow, and inter-procedural behavior of source code, and can find numerical, ...
  37. [37]
    [PDF] Polyspace Bug Finder – Identify software defects via static analysis
    Traceability from code to models. Polyspace Bug Finder and Polyspace Code Prover verification results, including MISRA analysis can be traced from code to ...Missing: simulation | Show results with:simulation
  38. [38]
    Code Metrics - MATLAB & Simulink - MathWorks
    You can choose to calculate statistics about your program. Use the Calculate code metrics (-code-metrics) analysis option to activate code metric checking.
  39. [39]
    MISRA C:2012 Directives and Rules - MATLAB & Simulink
    Polyspace can check your code against the MISRA C:2012 coding rules and some directives. The subgroups listed map to the different subsets outlined in the ...Missing: prioritization | Show results with:prioritization
  40. [40]
    Polyspace Code Prover User's Guide - DOKUMEN.PUB
    Dec 23, 2017 · CERT C Polyspace supports all statically enforceable rules in the CERT C standard. The standard categorizes the guidelines into rules and ...
  41. [41]
    Prioritize Check Review in Polyspace Access Web Interface
    Prioritize Check Review in Polyspace Access Web Interface. This example shows how to prioritize your check review. Try the following approach.
  42. [42]
    Prioritize Check Review - MATLAB & Simulink - MathWorks
    For easier review, run Polyspace® Bug Finder™ on your source code first. Once you address the defects that Polyspace Bug Finder finds, run Polyspace Code Prover ...
  43. [43]
    [PDF] DO-178C Workflow with Qualified Code Generation - MathWorks
    The DO-178C workflow includes qualified code generation, design checks, and support for testing, code generation, and certification, with source code ...
  44. [44]
    Integrate Polyspace as You Code in IDEs and Editors Without Plugins
    Polyspace as You Code supports these IDEs with extensions or plugins: Visual Studio, Visual Studio Code, and Eclipse. Even if an IDE is not explicitly ...Missing: CI/ Jenkins GitHub Jira
  45. [45]
    MathWorks Polyspace - Jenkins Plugins
    May 6, 2025 · The MathWorks Polyspace Plugin for Jenkins enables automated Polyspace analyses within Jenkins. Getting Started Step 1: Configure Plugin
  46. [46]
    Use Polyspace with Github Actions
    With GitHub® Actions, you can run a Polyspace® analysis on your C or C++ code as part of your workflow. Polyspace can identify run-time errors, concurrency ...
  47. [47]
    Create Bug Tracking Tool Tickets from the - Polyspace - Access
    If you use a bug tracking tool (BTT) such as Jira Software or Redmine as part of your software development process, you can configure Polyspace® Access to ...
  48. [48]
    Code Prover Analysis in Simulink - MathWorks
    Use Polyspace to identify potential bugs, runtime errors, and coding standard violations in your Simulink model.Missing: exploration | Show results with:exploration
  49. [49]
    Static Code Analysis in Continuous Integration and ... - MathWorks
    Continuous integration and delivery (CI/CD) is an extension of agile that is mainly focused on the tools and processes needed to integrate code and automate ...Missing: R2024a | Show results with:R2024a
  50. [50]
    [PDF] Space Software Validation using Abstract Interpretation
    INRIA has developed around 1993 a tool,. IABC, based on academic studies ... products, and industrialized by Polyspace Technologies during the following ...Missing: founded | Show results with:founded
  51. [51]
    Certification Standards - MATLAB & Simulink - MathWorks
    The DO-178C standard defines a set of objectives and activities for software to be approved for use in airborne systems. You can reduce risks and effort using ...Missing: proof | Show results with:proof
  52. [52]
    ISO 26262 Support in MATLAB and Simulink - MathWorks
    MATLAB and Simulink verification tools, and Polyspace code verification tools are certified by TÜV SÜD as qualified tools according to ISO 26262 for ASIL AD.
  53. [53]
    Volvo Cars Software Factory Increases Pace and Quality of ...
    With Polyspace, we can ensure software security and quality by identifying and fixing critical run-time errors before every code merge.Missing: case | Show results with:case
  54. [54]
    IEC 62304 standard for medical device software development
    The IEC 62304 standard specifies a set of processes, activities, and tasks that establish a common framework for designing safe and tested software for medical ...
  55. [55]
    Check for and Review Coding Standard Violations - MathWorks
    Specify the coding rules through Polyspace analysis options. When you run Bug Finder, the analysis looks for coding rule violations in addition to other checks.Missing: prioritization | Show results with:prioritization
  56. [56]
    Coding Standards and Code Metrics - MATLAB & Simulink
    Polyspace supports MISRA, AUTOSAR, CERT, and JSF coding rule sets, and custom rules. Code metrics like cyclomatic complexity are also available.
  57. [57]
    AUTOSAR C++14 Rules - MATLAB & Simulink - MathWorks
    AUTOSAR C++14 rules are a list of rules that Polyspace can check code against, including rules about unused variables, non-void return types, and unreachable  ...
  58. [58]
    https://www.mathworks.com/help/bugfinder/autosar-c-14.html
  59. [59]
    Polyspace Bug Finder - Common Weakness Enumeration
    Jun 7, 2018 · Polyspace Bug Finder users can filter defects by CWE identifiers. The procedure is detailed in the documentation.
  60. [60]
    Optimize Your Functional Safety Toolchain with MATLAB, Simulink ...
    Jun 27, 2023 · Optimize Your Functional Safety Toolchain with MATLAB, Simulink and Polyspace ... ISO 26262, SOTIF, IEC 61508, ISO 21434 and Automotive SPICE.