提高程式驗證自動化程度的技術

《提高程式驗證自動化程度的技術》是依託中國科學技術大學，由陳意雲擔任項目負責人的面上項目。

基本介紹

• 中文名：提高程式驗證自動化程度的技術
• 項目類別：面上項目
• 項目負責人：陳意雲
• 依託單位：中國科學技術大學

中文摘要

基於邏輯推理的程式驗證是提高軟體可信程度的一種重要方法。本項目研究促進程式驗證方法走向實用的技術和相關理論，重點解決指針類型給程式驗證帶來的障礙，為指針程式的自動驗證設計一種比較全面的解決辦法。.該項研究基於下面的思路：（1）程式驗證不必孤立地進行，可用程式分析收集的信息來支持程式驗證；（2）程式設計師可通過提供一些對程式分析和程式驗證有用的提示，來換取它們替程式設計師完成一些很有價值的事情；（3）在通過增強程式語言和斷言語言的表達能力來拓展程式驗證器的能力時，要儘量避免給自動定理證明器帶來太多的負擔。.本項目的研究基於上面的思路展開，預計主要亮點是：提出一種直接把形狀圖作為斷言的形狀圖邏輯，提出形狀系統概念。.本項目的研究幫助解決程式自動驗證的瓶頸問題，促進程式驗證的研究和套用的開展。

結題摘要

1．項目背景形式驗證是提高軟體可信程度的重要方法。其中一條途徑是演繹推理，它用形式方法對軟體進行數學推理。本項目從設計新的程式語言機制來提高合法程式的門檻，以排除部分有邏輯錯誤的程式；採用程式分析來收集程式信息，用這些信息來支持程式驗證等方法來研究安全C語言的自動程式驗證。 2．主要研究內容（1）面向自動程式驗證的C語言子集的設計。（2）在C語言中，面向易變數據結構的形狀系統的設計。（3）用於實現形狀系統的形狀圖邏輯的設計（4）安全C語言的規範語言SCSL（Safe C Specification Language）的設計（5）提升程式驗證器的證明能力的探索（6）設計並實現安全C語言的程式驗證器 3．重要結果（1）以禁止無法推斷的別名和限制可推斷的別名為指導思想，設計了一種面向自動程式驗證的安全C語言。（2）為易於驗證操作易變數據結構的程式，設計了面向易變數據結構的形狀系統以及相關的形狀圖邏輯。（3）定義了形狀圖的語法理論和語義理論，定義了形狀圖重寫系統及其終止性、局部合流性和合流性，提出了基於形狀圖重寫的形狀圖等價判定和蘊涵判定的方法。（4）設計了具有自己特色的、用於書寫函式前後條件和循環不變式等的安全C語言的規範語言SCSL。（5）實現了安全C語言程式驗證器的一個初步原型，已經能夠自動驗證百行左右的操作各類指針或數組的程式。 4．科學意義本項目研究促進基於演繹推理的程式驗證方法走向實用的技術和相關理論，重點解決了指針類型給程式驗證帶來的障礙，把程式驗證技術推進到能為用安全C語言寫的實際程式進行自動驗證的階段。