可信軟件前沿理論和技術(shù)ppt課件

1、可信軟件的前沿實(shí)際和技術(shù)可信軟件的前沿實(shí)際和技術(shù)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院中科大耶魯高可信軟件結(jié)合研討中心中科大耶魯高可信軟件結(jié)合研討中心邵中、陳意云、張昱、郭宇、李兆鵬等邵中、陳意云、張昱、郭宇、李兆鵬等 2019.7課課 程程 簡簡 介介 教學(xué)目的和根本要求教學(xué)目的和根本要求經(jīng)過引見經(jīng)過引見 高可信軟件研討領(lǐng)域中的國際前沿的實(shí)際和技高可信軟件研討領(lǐng)域中的國際前沿的實(shí)際和技術(shù)術(shù) 中科大耶魯高可信軟件結(jié)合研討中心的相關(guān)中科大耶魯高可信軟件結(jié)合研討中心的相關(guān)研討研討使同窗們使同窗們 對高可信軟件研討領(lǐng)域的實(shí)際和技術(shù)有初步了對高可信軟件研討領(lǐng)域的實(shí)際和技術(shù)有初步了解解 參與至少是關(guān)注

2、該領(lǐng)域的研討和開發(fā)任務(wù)參與至少是關(guān)注該領(lǐng)域的研討和開發(fā)任務(wù)并激發(fā)同窗們從事科研任務(wù)的熱情并激發(fā)同窗們從事科研任務(wù)的熱情課課 程程 簡簡 介介 課程主要內(nèi)容課程主要內(nèi)容預(yù)備知識預(yù)備知識 可信軟件研討領(lǐng)域的快速、全面的評述邵中可信軟件研討領(lǐng)域的快速、全面的評述邵中, 1 函數(shù)式編程言語、函數(shù)式編程和驗(yàn)證陳意云函數(shù)式編程言語、函數(shù)式編程和驗(yàn)證陳意云, 1 程序驗(yàn)證的邏輯根底邵中、郭宇，程序驗(yàn)證的邏輯根底邵中、郭宇，2前沿專題前沿專題 出具證明編譯器的構(gòu)造技術(shù)陳意云，出具證明編譯器的構(gòu)造技術(shù)陳意云，3 高可信軟件中的自動定理證明技術(shù)李兆鵬，高可信軟件中的自動定理證明技術(shù)李兆鵬，4 并行程序驗(yàn)證的實(shí)際和

3、方法張昱，并行程序驗(yàn)證的實(shí)際和方法張昱，5 國際上相關(guān)研討引見邵中，國際上相關(guān)研討引見邵中，6和和7課課 程程 簡簡 介介 課程實(shí)際安排：五個專題課程實(shí)際安排：五個專題 用用SML言語編寫函數(shù)式程序嚴(yán)肅，言語編寫函數(shù)式程序嚴(yán)肅，1 用定理證明輔助工具用定理證明輔助工具Coq學(xué)習(xí)邏輯推理王僖學(xué)習(xí)邏輯推理王僖, 2 用用Coq學(xué)習(xí)函數(shù)式程序的驗(yàn)證張昊中，學(xué)習(xí)函數(shù)式程序的驗(yàn)證張昊中，3 用用Coq完成一個簡單的命令式程序的驗(yàn)證完成一個簡單的命令式程序的驗(yàn)證 蔣蔣信予，信予，4和和5 用一階邏輯定理可滿足性檢查器用一階邏輯定理可滿足性檢查器Z3和出具證明和出具證明編譯器編譯器Ccomp進(jìn)展定理證明和程序驗(yàn)證嚴(yán)肅進(jìn)展定理證明和程序驗(yàn)證嚴(yán)肅，6 由結(jié)合研討中心的博士生指點(diǎn)課程實(shí)際由結(jié)合研討中心的博士生指點(diǎn)課程實(shí)際 課程實(shí)際地點(diǎn)：電三樓課程實(shí)際地點(diǎn)：電三樓517機(jī)房，機(jī)房，14:00開場開場課課 程程 簡簡 介介 課程調(diào)查課程調(diào)查 沒有考試，有課程實(shí)際調(diào)查沒有考試，有課程實(shí)際調(diào)查 每天最后一天除外下午有練習(xí)題，經(jīng)助教每天最后一天除外下午有練習(xí)題，經(jīng)助教驗(yàn)收后給出等級區(qū)分：優(yōu)、良、中、差驗(yàn)收后給出等級區(qū)分：優(yōu)、良、中、差 根據(jù)各天的調(diào)查成果給出本課程的成果根據(jù)各天的調(diào)查成果給出本課程的成果 本課程不同于平常的課程