今日頭條
官方微信
官方抖音
案例頻道北京廣利核系統工程有限公司 谷偉卿，張智慧，白濤，齊敏
摘要：同步數據流語言是一種廣泛應用于核電及其他安全關鍵領域的語言，在同步數據流語言到順序執行語言的翻譯轉換過程中，語義等價要保證賦值語句的左右值地址互不相交，這至關重要。本文使用形式化方法描述了翻譯過程中地址互不相交的性質，并通過定理證明的方式對其進行了驗證。基于本方法的編譯器在某核電站的安全保護系統中得到了應用。
關鍵詞：同步數據流；定理證明；Coq；語義等價；地址不相交
在線預覽：可信編譯器中地址不相交的保持性證明
摘自《自動化博覽》2017年4月刊
北京市公安局海淀分局備案號：11010802023656號