第一部分

Polyspace工作流程概覽

目標：了解Polyspace Bug Finder與Code Prover并跑通一個例子程序

·?Polyspace與軟件開發流程

·?簡單驗證樣例

·?分析代碼中的缺陷與運行時錯誤

Polyspace Bug Finder分析

目標：分析可能不符合ANSI C的代碼并配置運行時環境，使用 Bug Finder 糾正缺陷和編碼規則違規。

·?常見運行環境構件

·?處理處理器特定代碼

·?定義執行的上下文

·?設置目標硬件信息

·?分析和管理Bug Finder發現的缺陷

·?檢測編碼規則沖突

·?度量代碼統計指標

分析Polyspace Code Prover的結果

目標：?能熟練解釋Polyspace Code Prover的結果。

·?抽象解釋概覽

·?調用層次分析

·?源代碼導航

·?執行路徑

·?變量范圍

·?全局變量

代碼驗證中的檢查項

目標：能熟練解讀Polyspace Code Prover的結果。

·?C代碼檢查項一覽

·?源代碼中的檢查項定位

·?檢查項描述

·?相關驗證選項

第二部分

管理Polyspace Code Prover驗證與結果

目標：處理含有大量未證明檢查項的驗證結果。

·?判斷驗證開銷

·?進行快速評審

·?進行選擇性的橙色代碼評審

·?設置驗證精度

·?區分橙色檢查項優先級

·?評審橙色檢查項

增加Polyspace Code Prover驗證精度

目標：學習如何在用Polyspace Code Prover驗證代碼時處置缺失的代碼，以及如何對此施加影響從而產生更有意義的驗證結果。

·?魯棒性驗證與上下文驗證

·?函數打樁

·?數據范圍指定

·?手動打樁

集成分析

目標：學習如何管理復雜性日益增加的代碼驗證，以及如何解釋并比較集成分析與健壯性分析。

·?管理代碼模塊

·?用Bug Finder與Code Prover分析集成缺陷與編碼違規

·?導入注釋

完整應用分析

目標：回顧對整個應用進行完整驗證時的流程和選項。

·?創建應用級驗證工程

·?改善應用的驗證結果

·?發現并發訪問問題

·?對比健壯性驗證和上下文驗證

·?創建文檔

第三部分

實踐教學（選修）

目標：花時間來回顧你學到的內容并在你自己的項目上直接應用 Polyspace. 潛在內容包括：

·?Bug Finder 檢測

·?驗證 C++ 代碼

·?任務和共享數據分析

·?驗證生成的代碼

·?開發過程回顧

·?工作流程整合

·?客戶端/服務器軟件安裝

·?項目代碼的 Polyspace 配置

·?結果解釋