Polyspace Code Prover for C/C++ Code Verification


Strong knowledge of C or C++

Detailed course outline

Day 1 of 3
Introduction to Polyspace Verification

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

  • Overview of Polyspace Code Prover
  • Simple verification example
  • Remote verification using MATLAB Distributed Computing Server
Target Compilation Environment

Objective: Verify code that may not be ANSI C compliant and account for the run-time environment.

  • Common run-time environment artifacts
  • Handling processor-specific code
  • Defining the execution context
  • Setting target hardware information
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 variable
Function Stubbing and Data Range Specifications

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
  • Stubbing function inputs
Day 2 of 3
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 Orange Checks

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
  • Using Assistant Mode
Enforcing MISRA-C Compliance

Objective: Use Polyspace to check for MISRA-C compliance of source code.

  • Overview of the MISRA-C coding standard
  • Launching the MISRA-C checker
  • Reviewing MISRA-C checker results
  • Understanding the effects of MISRA-C standards on Polyspace Code Prover verification
Web Metrics and Reports

Objective: Use Web metrics to share and catalog verification results, and generate standard reports from verification results.

  • Sharing results
  • Using Web metrics
  • Testing software quality objectives
  • Creating documentation
Contextual Verification

Objective: Review procedures and options that are useful when verifying larger quantities of code.

  • Setting up a contextual verification
  • Improving the results of a contextual verification
  • Comparing robustness and contextual verification
Day 3 of 3
Hands-on Instruction

Objective: Spend time reviewing what you have learned and applying Polyspace Code Prover directly to your own project. Potential topics include:

  • Development process review
  • Workflow integration
  • Client/Server software installation
  • Polyspace configuration for project code
  • Results interpretation