典型文献
机械化验证一个高效的迭代数据流求解算法
文献摘要：
迭代计算数据流等式的解,是数据流分析的常用方法.计算支配节点,从而识别自然循环,是许多现代编译器优化分析的重要组成部分.机械化验证高效的求解支配节点的算法通常是获得一个实际的"验证编译器"不可或缺的一部分.为了形式化证明一个高效的迭代求解严格支配节点的算法(CHK),首先建立了值域是逆序列表集合的半格结构,逆序列表中的元素是控制流图中节点的逆后序遍历次序,并证明了它是一个半格,其偏序满足上升链条件.然后使用半格结构,实现了一个基于工作表的Kildall迭代算法,计算严格支配节点.接下来,首先给出了控制流图中支配节点的定义性规范和相关性质定理,然后构造并证明了迭代求解算法所满足的重要性质.利用这些性质定理,相对于定义性规范,证明了该迭代求解算法的正确性和完备性.最后进行总结,并讨论未来工作.整个形式化开发使用的是定理证明助手Isabelle/HOL.
文献关键词：
机械化验证;高效迭代算法;支配节点
中图分类号：
作者姓名：
江南;汪吕蒙;张晓瞳;何炎祥
作者机构：
湖北工业大学 计算机学院, 湖北 武汉 430068;武汉大学 计算机学院, 湖北 武汉 430072
文献出处：
引用格式：
[1]江南;汪吕蒙;张晓瞳;何炎祥-.机械化验证一个高效的迭代数据流求解算法)[J].软件学报,2022(06):2115-2126
A类：
机械化验证,支配节点,现代编译,CHK,Kildall,高效迭代算法
B类：
求解算法,迭代计算,算数,等式,数据流分析,常用方法,自然循环,编译器,优化分析,形式化证明,迭代求解,解严,值域,逆序,序列表,半格,控制流图,中节点,后序,遍历,历次,次序,一个半,偏序,工作表,接下来,中支,性质定理,完备性,未来工作,定理证明,助手,Isabelle,HOL
AB值：
0.329172
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
