欧美疯狂性受xxxxx喷水_可信編譯器中地址不相交的保持性證明-案例-控制網(wǎng)

可信編譯器中地址不相交的保持性證明

企業(yè)：北京廣利核系統工程有限公司領(lǐng)域：工業(yè)安全
點(diǎn)擊數：1772 發(fā)布時(shí)間：2017-04-25 08:35:20
分享到：

同步數據流語(yǔ)言是一種廣泛應用于核電及其他安全關(guān)鍵領(lǐng)域的語(yǔ)言，在同步數據流語(yǔ)言到順序執行語(yǔ)言的翻譯轉換過(guò)程中，語(yǔ)義等價(jià)要保證賦值語(yǔ)句的左右值地址互不相交，這至關(guān)重要。本文使用形式化方法描述了翻譯過(guò)程中地址互不相交的性質(zhì)，并通過(guò)定理證明的方式對其進(jìn)行了驗證?；诒痉椒ǖ木幾g器在某核電站的安全保護系統中得到了應用。

北京廣利核系統工程有限公司谷偉卿，張智慧，白濤，齊敏

摘要：同步數據流語(yǔ)言是一種廣泛應用于核電及其他安全關(guān)鍵領(lǐng)域的語(yǔ)言，在同步數據流語(yǔ)言到順序執行語(yǔ)言的翻譯轉換過(guò)程中，語(yǔ)義等價(jià)要保證賦值語(yǔ)句的左右值地址互不相交，這至關(guān)重要。本文使用形式化方法描述了翻譯過(guò)程中地址互不相交的性質(zhì)，并通過(guò)定理證明的方式對其進(jìn)行了驗證?；诒痉椒ǖ木幾g器在某核電站的安全保護系統中得到了應用。

關(guān)鍵詞：同步數據流；定理證明；Coq；語(yǔ)義等價(jià)；地址不相交

在線(xiàn)預覽：可信編譯器中地址不相交的保持性證明

摘自《自動(dòng)化博覽》2017年4月刊

1.我有以下需求：
得到貴公司產(chǎn)品詳細資料得到貴公司產(chǎn)品的價(jià)格信息貴公司產(chǎn)品銷(xiāo)售人員聯(lián)系我貴公司技術(shù)支持人員聯(lián)系我
2.詳細的需求：
*
姓名:	*
單位:
電話(huà):	*
郵件:	*

技術(shù)頻道

行業(yè)頻道

熱門(mén)頻道

技術(shù)頻道

行業(yè)頻道

熱門(mén)頻道

案例頻道

熱點(diǎn)新聞

推薦產(chǎn)品