PAR平臺中若干軟件構件形式化驗證技術研究

胡啟敏,薛錦云 ,游 珍,程 著

(1.江西師范大學國家網絡化支撐軟件國際科技合作基地，江西 南昌 330022;2.江西省高性能計算技術重點實驗室，江西 南昌 330022)

1 引言

PAR平臺[1 - 4]是本研究團隊在十多項國家級項目連續資助下，歷經二十多年潛心研究，最終研制成功的支撐軟件形式化和自動化開發的軟件平臺。PAR平臺的功能規約建模語言、抽象程序建模語言、軟件構件的設計充分體現了功能抽象和數據抽象的優越性，使得軟件開發變得便捷和可靠。利用PAR方法和PAR平臺，已經成功地形式化開發了諸多極具挑戰性的算法問題，包括：圖靈獎獲得者Knuth提出的二進制小數轉十進制小數算法[5,6]、圖平面性判定算法[7]、循環置換乘方的線性算法[8]等。

PAR平臺設計了豐富的可重用構件，包括“集合”“包”“序列”“樹”和“圖”等。這些構件是PAR平臺能夠實現便捷、可靠地開發軟件的關鍵要素。例如：在“集合”和“樹”構件支撐下，PAR平臺開發樹的前序遍歷問題僅需4行核心代碼；在“集合”和“圖”構件支撐下，PAR平臺開發圖的深度優先遍歷問題僅需5行核心代碼。在可重用軟件構件的支撐下，PAR平臺實現了軟件開發的簡潔性、便捷性和可靠性。同時，也使得確保軟件構件自身的正確性顯得尤為重要。

形式化驗證指驗證已有的系統(程序)是否滿足其規約的要求。常見的形式化驗證方法主要分兩類：演繹驗證(Deductive Verification)和模型檢測(Model Checking)。演繹驗證基于定理證明的基本思想，采用邏輯公式描述系統及其性質，通過一些公理或推理規則來證明系統具有某些性質。演繹驗證的過程一般需要通過定理證明器完成，它可以使用歸納的方法來處理無限狀態的問題。

目前，支持演繹驗證的定理證明工具有：法國國家信息與自動化研究院(INRIA)開發的Coq[9,10]、英國劍橋大學和德國慕尼黑大學開發的Isabelle[11]和美國康奈爾大學開發的Nuprl等。Coq 中的歸納類型擴展了傳統程序設計語言中有關類型定義的概念，融合遞歸類型和依賴積，具有很強的抽象能力和表達能力。相比之下，Isabelle等定理證明器表達能力較弱。

本文利用公理語義學中的Hoare公理系統，給出PAR平臺中若干可重用構件的形式語義；精確描述構件向外提供操作的功能。然后，通過形式化推導和循環不變式開發新技術，得到軟件構件相關操作所對應的循環不變式和實現程序。進而根據定理證明工具Coq抽象表示能力強等顯著特點，利用它提供的歸納類型、依賴積等機制，形式化地刻畫可重用構件實現程序以及相關循環不變式的屬性，對這些屬性能否滿足前后置斷言進行機械的、嚴格的推導和證明，從而驗證軟件構件的正確性。

2 基礎知識

2.1 PAR方法和PAR平臺

形式化方法PAR方法及其支撐平臺PAR平臺由功能規約和算法建模語言Radl(Recur-based algorithm design language)、泛型抽象程序建模語言Apla(Abstract programming language)、以及Radl模型到Apla模型自動生成系統、Apla模型到JAVA、C++、C#等可執行語言模型自動生成系統組成。

Radl語言用人們慣用的數學符號和書寫方式來描述算法規約、規約變換規則和算法。Radl作為Apla語言的前端語言，具有數學引用透明性。使用統一的格式(Qi:r(i):f(i))表示“在范圍r(i) 上，對函數f(i)施行q運算所得的量”，其中Q是q運算的一般化，可以是全稱量詞?、存在量詞?、求最小值量詞MIN、求最大值量詞MAX、求和量詞∑、求積量詞Π等，分別對應著的q運算是∧、∨、min、max、+、×等。利用這些量詞的性質可以進行規約變換。

Apla是Radl算法—Apla程序轉換器的目標語言，又是Apla到Dephi、Java、C++等可執行語言程序轉換器的源語言。設計Apla的主要宗旨是充分體現數據抽象、功能抽象、泛型等現代程序設計思想，使得構成的程序易于閱讀理解和驗證。

Apla的一個重要特色是它的泛型可重用構件庫，包括“集合”“包”“序列”“樹”和“圖”等。這些可重用構件庫的定義和實現，是課題組長期推導和證明各類程序的經驗總結，充分考慮了構件的簡潔性和通用性。例如：基于“序列”可重用構件，就可以便捷地構造隊列、堆棧等。

2.2 定理證明器Coq

Coq是法國INRIA研究院開發的一種基于高階邏輯的交互式定理證明工具，它使用規約語言Gallina表示程序、程序的屬性和這些屬性的證明。Coq系統主要由兩部分組成：證明開發系統和證明檢查器。證明開發系統類似于程序開發系統，擁有聲明模式和證明模式。在聲明模式里，程序員可以像設計程序一樣聲明變量、假設、公理；在證明模式里，程序員可以如同編寫程序一樣利用已聲明的對象和系統提供的證明策略構造引理或定理。證明檢查器用以驗證被形式化表示的程序，其核心是類型檢查算法，此算法通過檢查程序是否滿足程序規范來判定證明是否成立。

基于Coq形式化驗證程序的過程一般分為標注階段、形式化階段和證明階段。其中，標注階段完成對程序的前后置斷言、循環不變式、要證明的程序屬性的描述。形式化階段在Coq系統中采用形式化的方法完成對程序、標注的相關定義。證明階段根據形式化的程序、標注來抽取關于程序滿足相關屬性的定理，然后在Coq系統中對定理進行證明。

本文利用研究團隊在復雜算法程序形式化推導、求解問題的遞推關系式構造、循環不變式開發新技術等方面取得的研究成果，結合Hoare公理體系、Dijkstra最弱前置謂詞方法和Coq系統的自身特點，將基于Coq形式化驗證程序分為以下5個步驟：

(1)給出程序的形式化語義，即：給出程序前后置斷言的精確描述。

(2)從程序前后置斷言出發，進行形式化推導，找出程序求解的遞推關系式，并利用該遞推關系式和循環不變式開發新技術構造循環不變式ρ和具體實現程序。

(3)使用Coq系統的Gallina語言和歸納類型、遞歸類型和依賴積等機制，定義相關數據類型、數據結構以及相關函數；用Gallina語言描述第(2)步得到的循環不變式。

(4)給出程序應滿足相關屬性的定理，并用Gallina語言描述。如果用S表示程序語句，謂詞公式Q、R表示程序的前置和后置斷言，從S和R定義最弱前置謂詞WP(‘S’,R)。程序應滿足的定理即：Q→(WP(‘S’,R)。

如果程序中有循環語句，則要把Dijkstra最弱前置謂詞法中證明循環語句的五個蘊含表達式分別描述成Coq能夠識別的五個定理，如下所示：

Theoremwp1:Q→ρ//程序循環開始前ρ為真

Theoremwp2:ρ∧Ci→wp(‘Si’,ρ)/*每一次循環，ρ為真*/

Theoremwp3:ρ∧┐Guard→R//循環結束時，R為真

Theoremwp4:ρ∧Guard→τ> 0/*循環沒結束時，界函數大于0*/

Theoremwp5:ρ∧Ci→wp(‘τ1:=τ;Si’,τ<τ1)/*每一次循環，界函數的值減少*/

(5)利用Coq系統提供的證明規則和第(3)步定義的數據類型、數據結構和相關函數，證明第(4)步的定理。

3 “集合”構件的形式語義與驗證

無重復元素的一組同類型數據構成集合。集合構件可以通過數組或鏈表實現。用數組實現的集合，元素個數受限制，稱為有限集合；用鏈表實現的集合，元素個數無限制，稱為無限集合。

3.1 “集合”構件的形式語義

程序的形式語義主要有操作語義、指稱語義、代數語義、公理語義等4種。為便于驗證，本節給出構件各操作的公理語義；操作語義等限于篇幅，此處省略。 “集合”構件各個操作的公理語義如下(其中，前后置斷言采用Radl語言書寫，“集合”構件各操作的實現程序是否滿足前后置斷言，將在3.2節進行驗證)：

Type ADTset(elem:T,[SIZE:integer])

/*T表示集合元素是泛型的，可以是整型、字符型等。SIZE是可選項，如果有SIZE，指集合元素的個數不超過SIZE，該集合用數組實現。如果缺省SIZE，指集合元素沒有限制，該集合需要用鏈表實現。下文重點討論有限集合*/

Invariant: 0≤length≤SIZE;

Initially:set=nullset;

VarS:set,length:integer;

Operations:

Oneitemset(elem:T)/*Oneitemset操作可建立僅含一個元素的集合，’S表示操作執行后，集合對應的狀態，S[0]表示集合的首元素*/

Pre True

Post ‘S.length=1∧’S[0]=elem

Intersection(R:set) return(‘S:set)/*Intersection操作計算集合S與集合R的交集*/

Pre 0≤R.length

Post (?k:0≤k≤’S.length-1:‘S[k]∈S∧‘S[k]∈R)

Union(R:set) return(‘S:set)/*Union操作計算集合S與集合R的并集*/

Pre 0≤S.length+R.length

Post (?k: 0≤k≤’S.length-1: ‘S[k]∈S∨‘S[k]∈R)

Sub(R:set) return(‘S:set)/*Sub操作用于在集合S中去除在集合R中出現的元素*/

Pre 0≤R.length

Post (?k:0≤k≤’S.length-1: ‘S[k]∈S∧‘S[k] ?R)

Involve(elem:T)return(flag:Boolean)/*Involve操作用于判斷elem是否屬于集合S*/

PreTrue

Post(flag=true∧(?: 0≤k≤S.length-1: S[k]=elem) ∨(flag=false)

Include(R:set) return(flag:Boolean)/*Include操作用于判斷S是否是R的子集*/

PreS.length

Post (flag=true∧(?k: 0≤k≤S.length-1:S[k]∈R)) ∨(flag=false)

Equal(R:set) return(flag:Boolean)/*Equal操作用于判斷集合S與集合R是否相等*/

Pre 0≤R.length

Post (flag=true∧S.length=R.length∧(?k:0≤k≤S.length-1:S[k]∈R))∨(flag=false)

Copy(R:set)/*Copy操作用于將集合R替換為集合S*/

Pre 0≤R.length

Post ‘S.length=R.length∧(?k: 0≤k≤’S.length-1: ’S[k]=R[k])

3.2 “集合”構件的形式化驗證

“集合”構件提供了“求并集”“求交集”等7個操作。選取“集合”的判斷兩個集合是否存在子集關系的Include操作進行驗證。

(1)給出該操作的前后置斷言。

根據上文給出的Include操作的前后置斷言，假設集合S含m+1個元素，集合R含n+1個元素，可將后置斷言寫為：

Include(S[0..m],R[0..n]) ≡(i:0≤i≤m:(彐j:0≤j≤n:R[j]=S[i]))

(2)從程序后置斷言出發，進行形式化推導，找出程序求解的遞推關系式，構造循環不變式和求解程序。

利用量詞變換規則，作如下形式化推導，得出求解該操作的遞推關系式：

Include(S[0..m],R[0..n])

≡(i:0≤i≤m:(彐j:0≤j≤n:S[i]=R[j]))

{范圍分裂}

≡(i:0≤i≤m-1:(彐j:0≤j≤n:S[i]=R[j]))∧

(i:0≤i=m:(彐j:0≤j≤n:S[i]=R[j]))

{單點范圍}

≡(i:0≤i≤m-1:(彐j:0≤j≤n:S[i]=R[j]))∧

(彐j:0≤j≤n:S[m]=R[j])

{Include的定義}

≡Include(S[0..m-1],R[0..n])∧(彐j:0≤j≤n:S[m]=R[j])

用布爾類型變量flag表示Include(S[0..i],R[0..n]) 的值，即可得到循環不變式:

ρ：flag=Include(S[0..i],R[0..n]) ∧0≤i≤m

根據遞推關系和循環不變式，可得該操作的求解程序為：

i:=0;flag:=true;

WHILEi

BEGIN

IF notInvole(S[i],R[0..n])

THENflag:=false;RETURN

ELSEi:=i+1;

END.

(3)定義相關數據類型、數據結構以及相關函數。

利用Coq提供的歸納類型、遞歸和依賴積等抽象機制，定義Involve，Include如下：

FixpointInvolve(x:z,S:set):bool:=MatchSwith

|nil?false

|consyq?ifx=ythen true elseInvolvexq

FixpointInclude(S:set,R:set):bool:=MatchSwith

|nil?true

|consyq?ifInvolveyRthenIncludeqRelse false

同時，分別定義取集合S的第n個元素，和取集合S中前j個元素組成的子集如下：

Fixpointnth(n:z,S:set):z=matchSwith

|nil?default

|x::r? matchnwith

|0?x

|Sm?nthmrdefault

end.

end.

Fixpointupto(j:z,S:set):set =matchjwith

|0? matchswith

|nil?nil

|a::l?a::nil end

|Sn? matchswith

|nil?nil

|a::l?a::(firstnnl) end

end.

(4)給出程序應滿足相關屬性的定理。

利用上面定義的歸納類型和函數，證明循環不變式在每次循環執行前后均為真，如下所示：

首先給出首次執行循環，循環不變式為真的定理：

Theormwp1:

i=0∧Include(upto(0,S),R)

→Include(upto(i,S),R) ∧0≤i∧i

然后給出每次循環，循環不變式均為真的定理:

Theormwp2.1:

Include(upto(i,S),R)∧0≤i∧i

→Include(upto(suci,S),R) ∧0≤suci∧suci≤m

Theormwp2.2:

Include(upto(i,S),R)∧0≤i∧i

→negbInclude(upto(suci,S),R) ∧0≤i∧i

再給出當循環終止時，后置斷言為真的定理:

Theormwp3:

Include(upto(i,S),R) ∧0≤i∧i

→Include(upto(m-1,S),R)

循環的終止性證明的定理較為簡單，此處略。

(5)證明相關定理。

以上定理都可以在定理證明工具Coq中，使用“Induction”“Apply auto”等規則進行求證。

4 “包”構件的形式語義與驗證

允許重復元素的一組同類型數據構成包。包構件可以通過數組或鏈表實現。用數組實現的包，元素個數有限制，稱為有限包，用鏈表實現的包，元素個數無限制，稱為無限包。

4.1 “包”構件的形式語義

“包”的形式語義類似于集合，但由于“包”允許有重復元素，所以“包”的大部分操作規范不同于“集合”。給出“包”的公理語義如下：

Type ADTbag(elem:T,[SIZE:integer])

/*T表示包元素是泛型的，可以是整型、字符型等。SIZE是可選項，如果有SIZE，指包中元素的個數不超過SIZE，該包用數組實現。如果缺省SIZE，指包中元素沒有限制，該包需要用鏈表實現。下文重點討論有限包*/

Invariant: 0≤length≤SIZE;

Initially:bag=nullbag;

VarS:bag,length:integer;

Operations:

Oneitembag(elem:T)/*Oneitembag操作可建立僅含一個元素的包，’S表示操作執行后，包對應的狀態，S[0]表示包的首元素*/

Pre True

Post ‘S.length=1∧’S[0]=elem

Intersection(R:bag) return(‘S:bag)/*Intersection操作計算包S與包R的交集*/

Pre 0≤R.length

Post (?k:0≤k≤’S.length-1: ‘S[k]∈S∧‘S[k]∈R)

Union(R:bag) return(‘S:bag)/*Union操作計算包S與包R的并集，其中謂詞occ(x,S)表示x在包S中出現的次數*/

Pre 0≤S.length+R.length

Post ‘S.lengh=S.length+R.length∧

(?k: 0≤k≤’S.length-1:occ(‘S[k],’S)=occ(‘S[k],S)+occ(‘S[k],R))

Sub(R: bag)return(‘S: bag)/*Sub操作用于在包S中去除在包R中出現的元素*/

Pre0≤R.length

Post(?k:0≤k≤’S.length-1: ‘S[k]∈S∧‘S[k]?∈R)

Involve(elem:T) return(flag:Boolean)/*Involve操作用于判斷elem是否屬于包S*/

Pre True

Post (flag=true∧(?k: 0≤k≤S.length-1:S[k]=elem) ∨(flag=false)

Include(R:bag) return(flag:Boolean)/*Include操作用于判斷包S是否是R的子集，其中謂詞occ(x,S)表示x在包S中出現的次數*/

PreS.length

Post (flag=true∧(?k: 0≤k≤S.length-1:occ(S[k],S)≤occ(S[k],R)))∨(flag=false)

Equal(R:bag) return(flag:Boolean)/*Equal操作用于判斷包S與R是否相等，其中謂詞occ(x,S)表示x在包S中出現的次數*/

Pre 0≤R.length

Post (flag=true∧S.length=R.length∧

(?k:0≤k≤S.length-1:occ(S[k],S)=occ(S[k],R))∨(flag=false))

Copy(R:bag)//Copy操作用于將包R替換為S

Pre 0≤R.length

Post ‘S.length=R.length∧(?k: 0≤k≤’S.length-1: ’S[k]=R[k])

4.2 “包”構件的形式化驗證

“包”構件提供了“求包的并集”“求包的交集”等7個操作。選取“包”的判斷兩個“包”是否存在子集關系的Include操作進行驗證。

(1)給出該操作的前后置斷言。

根據上文給出的Include操作的前后置斷言，假設包S含m+1個元素，包R含n+1個元素，occ(x,S)表示x在包S中出現的次數，可將后置斷言形式寫為：

Include(S[0..m],R[0..n]) ≡

?(i: 0≤i≤S.length-1:occ(S[i],S)≤occ(S[i],R))

(2)從程序前后置斷言出發，進行形式化推導，找出程序求解的遞推關系式，構造循環不變式和求解程序。

利用量詞變換規則，作如下形式化推導，得出求解該操作的遞推關系式：

Include(S[0..m],R[0..n])

≡(i:0≤i≤m:occ(S[i],S)≤occ(S[i],R))

{范圍分裂}

≡(i:0≤i≤m-1:occ(S[i],S)≤occ(S[i],R) ∧

(i:0≤i=m:occ(S[i],S)≤occ(S[i],R))

{單點范圍}

≡(i:0≤i≤m-1:occ(S[i],S)≤occ(S[i],R)∧

occ(S[m],S)≤occ(S[m],R))

{Include的定義}

≡Include(S[0..m-1],R[0..n])∧occ(S[m],S)≤occ(S[m],R)

用布爾類型變量flag表示Include(S[0..i],R[0..n]) 的值，即可得到循環不變式:

ρ：flag=Include(S[0..i],R[0..n]) ∧0≤i≤m

根據遞推關系和循環不變式，可得該操作的求解程序為：

i:=0;flag:=true;

WHILEi

BEGIN

IF notocc(S[i],S)≤occ(S[i],R)

THEN flag:=false;RETURN

ELSEi:=i+1;

END.

(3)定義相關數據類型、數據結構以及相關函數。

定義歸納類型Occ，Include如下：

FixpointOcc(x:z,s:bag):z:=Matchswith

|nil?0

|consyq?letn:=Occ(x,q) in

Ifeq_decyxthenn+1 elsen.

FixpointInclude(S:bag,R:bag):bool:=MatchSwith

|nil?true

|consyq?Occ(y,S)≤Occ(y,R)∧IncludeqR

(4)給出程序應滿足相關屬性的定理。

首先給出首次執行循環，循環不變式為真的定理：

Theormwp1:

i=0∧Include(upto(0,S),R)

→Include(upto(i,S),R) ∧0≤i∧i

然后給出每次循環，循環不變式均為真的定理:

Theormwp2.1:

Include(upto(i,S),R)∧0≤i∧i

→Include(upto(suci,S),R) ∧0≤suci∧suci≤m

Theormwp2.2:

Include(upto(i,S),R) ∧0≤i∧i

→negbInclude(upto(suci,S),R) ∧0≤i∧i

再給出當循環終止時，后置斷言為真的定理:

Theormwp3:

Include(upto(i,S),R) ∧0≤i∧i

→Include(upto(m-1,S),R)

循環的終止性證明的定理較為簡單，此處略。

(5)證明相關定理。

以上定理都可以在定理證明工具Coq中，使用“Induction”“Apply auto”等規則進行求證。

5 相關研究工作

文獻[12，13]在Coq 中利用一階語法對C語言的語法進行描述，并基于歸納謂詞對C語言、中間語言以及目標語言的操作語義進行機械化。文獻[14]中提出了如何在Coq 中對內存模型和并行編譯的正確性進行證明。該編譯器的源語言為并行的Clight，目標語言為并行的x86 匯編語言。Ynot是Coq 的一個擴展庫，實現了分離邏輯。基于Coq 和Ynot，文獻[15]中實現了一個輕量級的、完全經過驗證的關系型數據庫管理系統(RDBMS)，RDBMS 的功能規范、具體實現以及該實現滿足規范要求的證明，都在Coq 中進行了書寫和驗證。文獻[16]將CompCert 項目的正確性驗證理念運用在硬件綜合設計上，為Fe-Si(Bluespec的簡化版)的高級硬件描述語言實現了一個驗證編譯器。

上述驗證工作主要集中在語義機械化、編譯過程驗證、關系數據庫和硬件系統驗證上。本文結合Coq系統特點和團隊在循環不變式方面的開發新技術，程序形式化推導上的技術優勢，強調循環不變式在形式化驗證中所起的關鍵作用，將基于Coq的形式化驗證過程分為5個主要步驟，并驗證了PAR平臺若干典型軟件構件的正確性。

6 結束語

PAR平臺中的可重用軟件構件是PAR平臺體現功能抽象和數據抽象特性，實現便捷、可靠開發軟件的關鍵因素。因此，這些軟件構件自身的正確性和可靠性顯得尤為重要。

本文利用Hoare公理系統對軟件構件進行形式化描述，給出了精確的語義。進而，利用定理證明器Coq提供的歸納類型等抽象表示機制刻畫軟件構件實現程序和對應循環不變式的屬性，利用Coq提供的命題演算、謂詞演算功能機械地證明實現程序是否滿足前后置斷言，從而實現形式化驗證軟件構件正確性的目標。

將在此工作基礎上，進一步探索如何給出PAR平臺Radl語言、Apla語言的完整語義，如何形式化刻畫Apla抽象程序到C++、Java等可執行程序自動生成系統的主要功能，進而利用Coq工具，形式化驗證PAR平臺程序自動生成系統關鍵功能的正確性。

[1] Xue J.A unified approach for developing efficient algorithmic programs[J].Journal of Computer Science and Technology,1997,12(4):314-329.

[2] Xue J.Two new strategies for developing loop invariants and their applications[J].Journal of Computer Science and Technology,1993,8(2):147-154.

[3] Xue Jin-yun. A practicable approach for formal development of algorithmic programs[C]∥Proc of the International Symposium on Future Software Technology,1999: 158-160.

[4] Xue Jin-yun.PAR method and its supporting platform [C]∥Proc of the 1st International Workshop on Asian Working Conference on Verified Software,2006:159-169.

[5] Xue J,Davis R.A derivation and proof of Knuth’ binary to decemal program[J].Software Concepts & Tools,1997,18(4):149-156.

[6] Xue J,Davis R.A simple program whose derivation and proof is also[C]∥Proc of the 1st IEEE International Conference on Formal Engineering Method(ICFEM’97),1997:1.

[7] Gries D, Xue Jin-yun. The hopcroft-tarjan planarity algorithm presentations and improvements:TR88-906[R].New York:Department of Computer Science, Cornell University,1998.

[8] Xue Jin-yun,David G.Developing a linear algorithm for cubing a cycle permutation[J].Science of Computer Programming,1998,11:161-165.

[9] The Coq proof assistant[EB/OL].[2014-01-01].http: ∥coq.inria.fr/.

[10] Bertot Y， Castéran P． Interactive theorem proving and program development-Coq’Art: The calculus of inductive constructions[M]．London,UK: Springer，2004．

[11] Nipkow T, Paulson L C, Wenzel M． Isabelle /HOL: A proof assistant for higher-order logic[M].London,UK: Springer,2002．

[12] Lero X.Formal verification of a realistic compiler[J].Communications of the ACM,2009,52(7):107-115．

[13] Boldo S,Jourdan J-H,Leroy X,et al.A formally verified C compiler supporting floating-point arithmetic[C]∥Proc of the 21st IEEE International Symposium on Computer Arithmetic,2013: 107-115.

[14] Evcik J, Vafeiadis V, Nardelli F Z,et al.Relaxed-memory concurrency and verified compilation[C]∥Proc of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,2011: 43-54．

[15] Malecha G, Morrisett G, Shinnar A,et al.Toward a verified relational database management system[C]∥Proc of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,2010: 237-248.

[16] Braibant T,Chlipala A.Formal verification of hardware synthesis[C]∥/Proc of the 25th International Conference on Computer Aided Verification,2013:213-228.