超长整数运算的PVS规范与验证

• 作者: 孙国栋 牛晋刚
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 超长整数运算 原型验证系统(PVS) 一致性验证 形式规范 定理证明
• 年，卷（期）: 2015,（3）
• 所属期刊栏目: 网络、通信、安全
• 页码范围: 93-97
• 页数: 5页
• 分类号: TP311.5
• 字数: 4941字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.1402-0408

摘要

超长整数的运算是现代密码系统的应用基础，运算的正确性关系到密码系统的应用价值。为了验证超长整数算法的设计与需求目标之间的一致性，利用原型验证工具PVS对算法的正确性进行了证明。在介绍了超长整数的加法和减法算法并分析了其设计思想之后，给出了超长整数及其算法的形式规范，通过把算法需要满足的性质描述为定理，将算法的一致性验证问题转化为逻辑定理证明的问题，在PVS定理证明器上完成了相关定理的证明，从而表明这些算法是满足设计需求的。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	孙国栋	北京工业大学计算机学院	7	48	4.0	6.0
2	牛晋刚	北京工业大学计算机学院	1	3	1.0	1.0