-
题名命令式动态规划类算法程序推导及机械化验证
- 1
-
-
作者
左正康
孙欢
王昌晶
游珍
黄箐
王唱唱
-
机构
江西师范大学数字产业学院
江西师范大学计算机信息工程学院
网络化支撑软件国家国际科技合作基地(江西师范大学)
-
出处
《软件学报》
EI
CSCD
北大核心
2024年第9期4218-4241,共24页
-
基金
国家自然科学基金(62262031)
江西省自然科学基金(20232BAB202010,20212BAB202018)
+1 种基金
江西省教育厅科技项目(GJJ210307,GJJ210333,GJJ2200302)
江西省主要学科学术与技术带头人培养项目(20232BCJ22013)。
-
文摘
动态规划是一种递归求解问题最优解的方法,主要通过求解子问题的解并组合这些解来求解原问题.由于其子问题之间存在大量依赖关系和约束条件,所以验证过程繁琐,尤其对命令式动态规划类算法程序正确性验证是一个难点.基于动态规划类算法Isabelle/HOL函数式建模与验证,通过证明命令式动态规划类算法程序与其的等价性,避免证明正确性时处理复杂的依赖关系和约束条件,提出命令式动态规划类算法程序设计框架及其机械化验证.首先,根据动态规划类算法的优化方法(备忘录方法)和性质(最优子结构性质和子问题重叠性质)描述问题规约、归纳递推关系式和形式化构造出循环不变式,并且基于递推关系式生成IMP(minimalistic imperative programming language)代码;其次,将问题规约、循环不变式和生成的IMP代码输入VCG(verification condition generator),自动生成正确性的验证条件;然后,在Isabelle/HOL定理证明器中对验证条件进行机械化验证.算法首先设计为命令式动态规划类算法的一般形式,并进一步实例化得到具体算法.最后,例证所提框架的有效性,为动态规划类算法的自动化推导和验证提供参考价值.
-
关键词
Isabelle/HOL
机械化验证
动态规划
命令式
VCG
-
Keywords
Isabelle/HOL
mechanized verification
dynamic programming
imperative
verification condition generator(VCG)
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名Trie+结构函数式建模、机械化验证及其应用
- 2
-
-
作者
左正康
柯雨含
黄箐
王玥坤
曾志城
王昌晶
-
机构
江西师范大学计算机信息工程学院
-
出处
《软件学报》
EI
CSCD
北大核心
2024年第9期4242-4264,共23页
-
基金
国家自然科学基金(62262031)
江西省自然科学基金(20232BAB202010)
+1 种基金
江西省教育厅科技重点项目(GJJ210307,GJJ2200302)
江西省主要学科学术与技术带头人培养项目(20232BCJ22013)。
-
文摘
Trie结构是一种使用搜索关键字来组织信息的搜索树,可用于高效地存储和搜索字符串集合.Nipkow等人给出了实现Trie的Isabelle建模与验证,然而其Trie在存储和操作时存在大量的冗余,导致空间利用率不高,且仅考虑英文单模式下查找.为此,基于索引即键值的思想提出了Trie+结构,相较于传统的索引与键值分开存储的结构能减少50%的存储空间,大大提高了空间利用率.并且,对Trie+结构的查找、插入、删除等操作给出了函数式建模及其严格的机械化验证,保证操作的正确性和可靠性.进一步,提出一种匹配算法的通用验证规约,旨在解决一系列的匹配算法正确性验证问题.最后,基于Trie+结构与匹配算法通用验证规约,建模和验证了函数式中英文混合多模式匹配算法,发现并解决了现有研究中的基于完全哈希Trie的多模式匹配算法的模式串前缀终止的Bug.该Trie+结构以及验证规约在提高Trie结构空间利用率和验证匹配算法中,有一定的理论和应用价值.
-
关键词
Trie+
函数式建模
机械化验证
多模式匹配算法
-
Keywords
Trie+
functional modeling
mechanized verification
multi-pattern matching algorithm
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名机械化验证一个高效的迭代数据流求解算法
- 3
-
-
作者
江南
汪吕蒙
张晓瞳
何炎祥
-
机构
湖北工业大学计算机学院
武汉大学计算机学院
-
出处
《软件学报》
EI
CSCD
北大核心
2022年第6期2115-2126,共12页
-
基金
国家自然科学基金(61972293)
国家留学基金委地方合作项目(201808420414)。
-
文摘
迭代计算数据流等式的解,是数据流分析的常用方法.计算支配节点,从而识别自然循环,是许多现代编译器优化分析的重要组成部分.机械化验证高效的求解支配节点的算法通常是获得一个实际的“验证编译器”不可或缺的一部分.为了形式化证明一个高效的迭代求解严格支配节点的算法(CHK),首先建立了值域是逆序列表集合的半格结构,逆序列表中的元素是控制流图中节点的逆后序遍历次序,并证明了它是一个半格,其偏序满足上升链条件.然后使用半格结构,实现了一个基于工作表的Kildall迭代算法,计算严格支配节点.接下来,首先给出了控制流图中支配节点的定义性规范和相关性质定理,然后构造并证明了迭代求解算法所满足的重要性质.利用这些性质定理,相对于定义性规范,证明了该迭代求解算法的正确性和完备性.最后进行总结,并讨论未来工作.整个形式化开发使用的是定理证明助手Isabelle/HOL.
-
关键词
机械化验证
高效迭代算法
支配节点
-
Keywords
mechanized verification
efficient iterative algorithm
dominators
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
