[1] 钱振江,刘苇,黄皓. 操作系统形式化设计与验证综述[J]. 计算机工程, 2012,38(11):234-238.
[2] 钱振江. 安全操作系统形式化设计与验证方法研究[D]. 南京:南京大学, 2013.
[3] Elphinstone K, Klein G, Derrin P, et al. Towards a practial, verified kernel[C]// Proceedings of the 11th Workshop on Hot Topics in Operating Systems. 2007:Article No. 20.
[4] Berier W R, Hunt W A, Moore J S, et al. An approach to systems verification[J]. Journal of Automated Reasoning, 1989,5(4):411-428.
[5] Shao Zhong. Certified software[J]. Communications of the ACM, 2010,53(12):56-66.
[6] Reason J. Human Error[M]. Combridge University Press, 1990.
[7] Paulson L C. The foundation of a generic theorem prover[J]. Journal of Automated Reasoning, 1989,5(3):363-397.
[8] Paulson L C. Isabelle: A Generic Theorem Prover[M]. Springer, 1994.
[9] Hoare C A R. An axiomatic basis for computer programming[J]. Communications of the ACM, 1969,12(10):576-580.
[10]顾伟灏. 基于Isabelle的汇编指令模拟系统及其自动化翻译辅助验证工具[D]. 南京:南京大学, 2014.
[11]Intel Corporation. Inter 64 and IA-32 Architectures Software Developers Manual Vol.1[R]. Intel Corporation, 2004.
[12]Intel Corporation. Inter 64 and IA-32 Architectures Software Developers Manual Vol.2B[R]. Intel Corporation, 2012.
[13]Doron P, Patrizio P, Paola S. Model Checking[M]. Wiley Encyclopedia of Computer Science and Engineering, 2009.
[14]黄达明. 基于循环分析的程序验证技术研究[D]. 南京:南京大学, 2013.
[15]Cormen T H, Leiserson C E, 等. 算法导论[M]. 2版. 潘金贵,顾铁成,等译. 北京:机械工业出版社, 2006.
[16]Wenzel M. The Languages of Isabelle: Isar, ML, and Scala[EB/OL]. http://www4.in.tum.de/~wenzelm/papers/lausanne2009.pdf, 2009-09-01.
[17]Wenzel M. Isar: A Generic Interpretative Approach to Readable Formal Proof Documents[M]. Springer Berlin Heidelberg, 1999.
|