可信軟件的前沿理論和技術

1、可信軟件的前沿理論和技術可信軟件的前沿理論和技術計算機科學與技術學院計算機科學與技術學院中科大耶魯高可信軟件聯(lián)合研究中心中科大耶魯高可信軟件聯(lián)合研究中心邵中、陳意云、張昱、郭宇、李兆鵬等邵中、陳意云、張昱、郭宇、李兆鵬等 2010.7課課 程程 簡簡 介介 教學目標和基本要求教學目標和基本要求通過介紹通過介紹 高可信軟件研究領域中的國際前沿的理論和技術高可信軟件研究領域中的國際前沿的理論和技術 中科大耶魯高可信軟件聯(lián)合研究中心的相關研究中科大耶魯高可信軟件聯(lián)合研究中心的相關研究使同學們使同學們 對高可信軟件研究領域的理論和技術有初步了解對高可信軟件研究領域的理論和技術有初步了解 參與（至少是關

2、注）該領域的研究和開發(fā)工作參與（至少是關注）該領域的研究和開發(fā)工作并激發(fā)同學們從事科研工作的熱情并激發(fā)同學們從事科研工作的熱情課課 程程 簡簡 介介 課程主要內容課程主要內容預備知識預備知識 可信軟件研究領域的快速、全面的評述（邵中可信軟件研究領域的快速、全面的評述（邵中, 1） 函數(shù)式編程語言、函數(shù)式編程和驗證（陳意云函數(shù)式編程語言、函數(shù)式編程和驗證（陳意云, 1） 程序驗證的邏輯基礎（邵中、郭宇，程序驗證的邏輯基礎（邵中、郭宇，2）前沿專題前沿專題 出具證明編譯器的構造技術（陳意云，出具證明編譯器的構造技術（陳意云，3） 高可信軟件中的自動定理證明技術（李兆鵬，高可信軟件中的自動定理證明技

3、術（李兆鵬，4） 并行程序驗證的理論和方法（張昱，并行程序驗證的理論和方法（張昱，5） 國際上相關研究介紹（邵中，國際上相關研究介紹（邵中，6和和7）課課 程程 簡簡 介介 課程實踐安排：五個專題課程實踐安排：五個專題 用用sml語言編寫函數(shù)式程序（莊重，語言編寫函數(shù)式程序（莊重，1） 用定理證明輔助工具用定理證明輔助工具coq學習邏輯推理（王僖學習邏輯推理（王僖, 2） 用用coq學習函數(shù)式程序的驗證（張昊中，學習函數(shù)式程序的驗證（張昊中，3） 用用coq完成一個簡單的命令式程序的驗證完成一個簡單的命令式程序的驗證 （蔣信（蔣信予，予，4和和5） 用一階邏輯定理可滿足性檢查器用一階邏輯定理可滿足性檢查器z3和出具證明編和出具證明編譯器譯器ccomp進行定理證明和程序驗證（莊重，進行定理證明和程序驗證（莊重，6） 由聯(lián)合研究中心的博士生指導課程實踐由聯(lián)合研究中心的博士生指導課程實踐 課程實踐地點：電三樓課程實踐地點：電三樓517機房，機房，14:00開始開始課課 程程 簡簡 介介 課程考查課程考查 沒有考試，有課程實踐考查沒有考試，有課程實踐考查 每天（最后一天除外）下午有練習題，經(jīng)助教驗收每天（最后一天除外）下午有練習題，經(jīng)助教驗收后給出等級區(qū)分：優(yōu)、良、中、差后給出等級區(qū)分：優(yōu)、良、中、差 根據(jù)各天的考查成績給出本課程的成績根據(jù)各天的考查成績給出本課程的成績 本課程不同于平時