可信软件代码中程序标注的使用及类型验证

摘要：

程序标注技术能够勾勒程序代码中的各种数据属性和软件行为,提出了使用许可类型系统作为沟通程序标注和程序代码的桥梁.从程序代码的角度分析和验证了程序的安全性,进而提升了整个软件系统的可靠性和可维护性.

关键词：可信代码、程序标注、程序验证

所属期刊栏目：35

分类号：TP311.53(计算技术、计算机技术)

资助基金：国家自然科学基金60850002;高等学校博士学科点专项科研基金20093219120026;南京理工大学科技发展基金XKF09017

在线出版日期：2010-09-17（万方平台首次上网日期，不代表论文的发表时间）

页码：570-573