由一阶逻辑公式得到命题逻辑可满足性问题实例

命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为 SAT 问题.为了利用现有的高效 SAT工具,提出了一种从一阶逻辑公式生成 SAT 问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题.

韩国加密标准的安全性分析

SEED是韩国的数据加密标准，设计者称用线性密码分析攻击SEED的复杂度为2^335.4，而用本文构造的15轮线性逼近攻击SEED的复杂度为2^328．为了说明SEED抵抗差分密码分析的能力，设计者首先对SEED的变体SEED‘做差分密码分析，指出9轮SEED*对差分密码分析是安全的；利用SEED^*的扩散置换和盒子的特性，本文构造SEED^*的9轮截断差分，因此10轮SEED^*对截断差分密码分析是不免疫的．本文的结果虽然对SEED的实际应用构成不了威胁，但是显示了SEED的安全性并没有设计者所称的那样安全．

多线程程序数据竞争的静态检测

多线程并发程序的广泛使用带来了更多的数据竞争错误．传统的数据竞争静态检测由于对并发语义和别名信息的保守分析会导致很多假错误．因此，提出了一个精确有效的静态检测框架：分析应用了精确的别名分析并静态模拟了访问事件发生序；为提高分析效率，检测算法提出了一个以对象为中心，结合Escape分析缩小检测范围的检测算法并配合设计了压缩的别名等价类表示．检测框架在一个静态Java编译器JTool上做了实现，对于测试程序取得了很好的分析结果．

基于实时数据库的卫星测试平台的设计与实现

卫星测试数据的有效存储与展现对卫星测试有着重要的意义,同时随着卫星技术的发展,一颗卫星的多阶段测试,多颗卫星同时测试是不可避免的。而及时有效的处理测试产生大量的实时数据将是极大的挑战。设计并实现了基于实时数据库的分布式卫星测试平台,可以有效地管理多颗卫星的测试,同时结合ACE框架的通讯结构可以有效的对测试间内外的测试人员提供实时的数据监视与精确的历史查询统计。

石油化工行业生产执行系统应用研究

分析了国内外石油化工行业生产执行系统的特点,采用分布对象技术,提出了灵活的可组态的生产执行系统体系结构,该体系结构主要由数据平台、业务逻辑和用户界面3个层次构成;针对物料平衡与数据整合的关键问题,提出了基于多维物料移动模型的多层递阶平衡方法;结合石油化工行业的业务知识和领域知识,设计开发了一个炼化一体化的生产执行软件系统--石油化工企业生产执行系统,并在典型企业进行了应用验证.