| [1] |
梅妍.结构化测试在MIS软件性能验证中的应用研究[D].上海:复旦大学,2011.
|
| [2] |
郑红军,张乃孝.软件开发中的形式化方法[J].计算机科学,1997,24(6):90-96.
|
| [3] |
王戟,李宣东.形式化方法与工具专刊前言[J].软件学报,2011,22(6):1121-1122.
|
| [4] |
傅育熙,李国强,田聪.形式化方法的理论基础专题前言[J].软件学报,2018,29(6):1049-1050.
|
| [5] |
王戟,詹乃军,冯新宇,等.形式化方法概貌[J].软件学报,2019,30(1):33-61.
|
| [6] |
卜磊,解定宝.混成系统形式化验证[J].软件学报,2014,25(2):219-233.
|
| [7] |
游珍,薛锦云.基于Isabelle定理证明器算法程序的形式化验证[J].计算机工程与科学,2009,31(10):85-89.
|
| [8] |
谯婷婷,王乐,王芳,等.基于Coq的软件安全性验证[J].计算机应用,2012,32(2):96-100.
|
| [9] |
张杰,王少超,关永.基于形式化方法的有限域乘法器的建模与验证[J].电子技术应用,2018(1):109-113.
|
| [10] |
KLEIN G,ELPHINSTONE K,HEISER G,et al.SeL4:formal verification of an OS kernel[C]//Proceedings of the 22nd ACM SIGOPS Symposium on Operating Systems Principles.New York,USA:ACM Press,2009:207-220.
|
| [11] |
BECKERT B,MOSKAL M.Deductive verification of system software in the verisoft XT project[J].KI-Künstliche Intelligenz,2010,24(1):57-61.
|
| [12] |
DAUM M,DORRENBACHER J,BOGAN S.Model stack for the pervasive verification of a microkernel-based operating system[C]//Proceedings of the 5th IEEE International Verification Workshop.Washington D.C.,USA:IEEE Press,2008,372:56-70.
|
| [13] |
GU Liang,VABNBERG A,FORD B,et al.CertiKOS:a certified kernel for secure cloud computing[C]//Proceedings of the 2nd Asia-Pacific Workshop on Systems.New York,USA:ACM Press,2011:3.
|
| [14] |
XU Fengwei,FU Ming,FENG Xinyu,et al.A practical verification framework for preemptive OS kernels[C]// Proceedings of International Conference on Computer Aided Verification.Berlin,Germany:Springer,2016:59-79.
|
| [15] |
陈丽蓉,李允,罗蕾.嵌入式操作系统的形式化验证研究[J].计算机科学,2015,42(8):203-214.
|
| [16] |
陈钢,于林宇,裘宗燕,等.基于逻辑的形式化验证方法:进展及应用[J].北京大学学报(自然科学版),2016,52(2):363-373.
|
| [17] |
张恒若,付明.基于Z3的Coq自动证明策略的设计和实现[J].软件学报,2017,28(4):819-826.
|
| [18] |
LEINO K R M.Dafny:an automatic program verifier for functional correctness[C]//Proceedings of International Conference on Logic for Programming Artificial Intelligence and Reasoning.Berlin,Germany:Springer,2010:348-370.
|
| [19] |
BOND B,HAWBLITZEL C,KAPRITSOS M,et al.Vale:verifying high-performance cryptographic assembly code[C]//Proceedings of IEEE USENIX Security Sympo-sium.Washington D.C.,USA:IEEE Press,2017:158-169.
|
| [20] |
何炎祥,吴伟,陈勇,等.基于SMT求解器的路径敏感程序验证[J].软件学报,2012,23(10):2655-2664.
|
| [21] |
胡凯.智能合约的形式化验证方法[J].信息安全研究,2016,12(2):1080-1089.
|
| [22] |
NELSON L,SIGURBLARNARSON H,ZHANG Kaiyuan,et al.Hyperkernel:push-Button verification of an OS kernel[C]//Proceedings of the 26th Symposium on Operating Systems Principles.New York,USA:ACM Press,2017:252-269.
|
| [23] |
郝耀辉,郭渊博,罗婷,等.基于Hoare逻辑的密码软件形式化验证系统[J].计算机工程,2012,38(3):121-123.
|
| [24] |
钱振江,黄皓,宋方敏.操作系统汇编级形式化设计和验证方法[J].软件学报,2016,27(12):3143-3157.
|
| [25] |
BEYER D.Competition on software verification (SV-COMP)[EB/OL].[2018-10-16].https://sv-comp.sosy-lab.org/2018/.
|
| [26] |
LI Jiaying,SUN Jun,LI Li,et al.Automatic loop-invariant generation and refinement through selective sampling[C]//Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering.Washington D.C.,USA:IEEE Press,2017:782-792.
|
| [27] |
BOUNOV D,DEROSSI A,MENARINI M,et al.Inferring loop invariants through gamification[C]//Proceedings of the 2018 Conference on Human Factors in Computing Systems.Montreal,Canada:[s.n.],2018:231.
|
| [28] |
XIE Xiaofei,CHEN Bihuan,ZOU Liang,et al.Automatic loop summarization via path dependency analysis[J].IEEE Transactions on Software Engineering,2018(99):1.
|