基于Z3的Coq自动证明策略的设计和实现

形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高;而使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.结合上述两种方式的优点,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减少了用户手动验证程序的开销.

基于PyExZ3的Web攻击流量的采集和分类

目前网络上有海量的攻击流量时刻威胁着Web应用的安全。要想直接对攻击流量进行有效搜集并分析难度很大,而要想通过搭建靶机的方式来搜集也十分费时费力且效率低下。针对上述问题,采用符号执行技术,在开源符号执行引擎PyExZ3的基础上,运用循环优化方法和对符号执行基础类型的完善,弥补了PyExZ3的不足,使得改进后的原型系统能够高效可靠地对绝大部分基于Python的Web攻击脚本进行自动化分析。

基于SMT的机组排班问题优化求解

机组排班是航空公司运营计划非常重要的一个环节,合理的机组排班可以为航空公司省下一大笔机组成本支出,从而增加航空公司的收益.由于机组排班过程涉及大量的复杂约束,属于NP难问题,因此优化求解困难.本文提出了一种基于可满足性模理论(Satisfiability Modulo Theories,SMT)的航空公司机组排班问题的优化求解方法,将机组排班过程中的各种约束转化为一阶逻辑公式,设立求解目标为最小化成本和最大化机组利用率,将问题转化为求在给定逻辑公式可满足情况下的最优解,并利用SMT求解器Z3进行求解.实验表明,本文的算法能有效的求解一定规模航班计划的机组排班问题,给航空公司带来一定的收益.

基于SMT的不完全信息游戏求解

不完全信息博弈是人工智能领域的一个重要研究领域.本文提出了一种基于可满足性模理论(Satisfiability Modulo Theories, SMT)的不完全信息游戏求解方法,首先通过情景演算将游戏动态过程描述成对应的约束,并将约束编写成命题逻辑公式,然后将推理问题转化为逻辑公式可满足性问题,调用SMT求解器Z3进行求解.应用表明,本文的算法能有效地推理出游戏的正确结果.