小型微型计算机系统
小型微型計算機繫統
소형미형계산궤계통
MINI-MICRO SYSTEMS
2011年
7期
1400-1405
,共6页
规范转换%代码优化%数据流分析%出具证明编译器
規範轉換%代碼優化%數據流分析%齣具證明編譯器
규범전환%대마우화%수거류분석%출구증명편역기
出具证明编译器在软件安全研究得到越来越多的关注,是程序验证研究的一个重要方向.但目前关于出具证明编译器的研究主要是在程序逻辑设计和定理自动化证明方面,很少关注编译优化对规范的影响.而编译优化是决定出具证明编译器是否能走向应用的关键因素之一.通过研究数据流优化的基本行为,提出利用数据流分析结果来变换规范的方法,以使原规范的约束准确而充分地施加于优化后的代码,并实现了一个包含多种优化和相应规范转换的编译器原型系统,展示了方法的可行性.
齣具證明編譯器在軟件安全研究得到越來越多的關註,是程序驗證研究的一箇重要方嚮.但目前關于齣具證明編譯器的研究主要是在程序邏輯設計和定理自動化證明方麵,很少關註編譯優化對規範的影響.而編譯優化是決定齣具證明編譯器是否能走嚮應用的關鍵因素之一.通過研究數據流優化的基本行為,提齣利用數據流分析結果來變換規範的方法,以使原規範的約束準確而充分地施加于優化後的代碼,併實現瞭一箇包含多種優化和相應規範轉換的編譯器原型繫統,展示瞭方法的可行性.
출구증명편역기재연건안전연구득도월래월다적관주,시정서험증연구적일개중요방향.단목전관우출구증명편역기적연구주요시재정서라집설계화정리자동화증명방면,흔소관주편역우화대규범적영향.이편역우화시결정출구증명편역기시부능주향응용적관건인소지일.통과연구수거류우화적기본행위,제출이용수거류분석결과래변환규범적방법,이사원규범적약속준학이충분지시가우우화후적대마,병실현료일개포함다충우화화상응규범전환적편역기원형계통,전시료방법적가행성.
