Polyspace for C/C++ Code Verification

Learn to analyze and verify C code for unsafe constructs, coding rule compliance, and run-time errors

TechSource Systems Pte Ltd


This two-day course discusses the use of Polyspace® Code Prover™ to prove code correctness, improve software quality metrics, and ensure product integrity. This hands-on course is intended for engineers who develop software or models targeting embedded systems.

Topics include:

  • Creating a verification project
  • Reviewing and understanding verification results
  • Emulating target execution environments
  • Handling missing functions and data
  • Managing unproven code (color-coded in orange by Polyspace products)
  • Applying MISRA-C® rules
  • Reporting analysis results
TechSource Systems Pte Ltd

Who Should

Engineers who develop software and model for embedded system target.

TechSource Systems Pte Ltd


Strong knowledge of C or C++

TechSource Systems Pte Ltd


Upon the completion of this training, attendee will be able to:

  • Verify a basic C file and view verification results
  • Verify code that contains deviations from ANSI standard
  • Set verification options that properly emulate the code’s target environment
  • Analyze code verification results
  • Create a stub for a missing function
  • Restrict range of function inputs, missing function outputs, and global
    variables for use in code verification
  • Identify verification options that affect specific types of verification checks
  • Prioritize unproven verification results based upon severity and verification accuracy
  • Use automated methods to review verification results.
  • Analyze source code for MISRA-C violations
  • Share verification results and justification with others
  • Interpret code verification results properly when an automatically generated
    main function is not used


TechSource Systems Pte Ltd
TechSource Systems Pte Ltd

TechSource Systems is MathWorks Authorised Reseller and Training Partner

Upcoming Program

  • Please keep me posted on the next schedule
  • Please contact me to arrange customized/ in-house training

Course Outline

Polyspace Workflow Overview

Objective: Become familiar with Polyspace Bug Finder and Polyspace Code Prover and work through an introductory example.

  • Software development workflows with Polyspace
  • Simple verification example
  • Analyzing defects and run-time errors
TechSource Systems Pte Ltd
TechSource Systems Pte Ltd

Polyspace Bug Finder Analysis

Objective: Analyze code that may not be ANSI C compliant and account for the run-time environment, and correct defects and coding rule violations using Polyspace Bug Finder.

Measuring code metrics

  • Common run-time environment artifacts
  • Handling processor-specific code
  • Defining the execution context
  • Setting target hardware information
  • Analyzing and managing Polyspace Bug Finder defects
  • Detecting coding rule violations

Analyzing Polyspace Code Prover Results

Objective: Become proficient at interpreting Polyspace Code Prover results.

  • Overview of abstract interpretation
  • Call tree analysis
  • Source code navigation
  • Execution paths
  • Variable ranges
  • Global variables
TechSource Systems Pte Ltd
TechSource Systems Pte Ltd

Code Verification Checks

Objective: Find run-time errors using diagnostics available in Polyspace Code Prover.

  • Overview of C source code checks
  • Location of checks in source code
  • Description of checks
  • Relevant verification options

Managing Polyspace Code Prover Verifications and Results

Objective: Handle verification results that contain large amounts of unproven checks.

  • Determining verification effort
  • Performing a quick review
  • Performing a selective orange review
  • Setting verification precision
  • Prioritizing orange checks
  • Reviewing orange checks
TechSource Systems Pte Ltd
TechSource Systems Pte Ltd

Adding Precision to Polyspace Code Prover Verifications

Objective: Learn how Polyspace Code Prover treats missing code during verification, and how to affect this behavior to produce more meaningful verifications.

  • Robustness verification and contextual verification
  • Function stubbing
  • Data range specification
  • Manual stubbing

Integration Analysis

Objective: Learn how to manage verifications with increasing code complexity, and how to interpret and compare integrated analysis with robust analysis.

  • Managing code modules
  • Analyzing integration defects and rule violations with Polyspace Bug
  • Finder and Polyspace Code Prover
  • Importing comments
TechSource Systems Pte Ltd
TechSource Systems Pte Ltd

Application Analysis

Objective: Review procedures and options that are useful when verifying complete applications.

  • Setting up an application verification
  • Improving the results of an application verification
  • Detecting concurrency issues
  • Comparing robustness and contextual verification
  • Creating documentation