自动推理系统研发平台
该平台主要研究原创的基于矛盾体分离的动态自动演绎推理理论与方法，并研发相应的自动推理系统。
1. 原创的自动推理理论体系
建立了原创的基于矛盾体分离的动态自动演绎推理理论与方法，形成了一种先进的基于逻辑演绎的自动推理科学体系，其成果具国际领先水平。
2. 命题逻辑问题求解系统
基于原创的自动推理理论体系，设计了22个命题逻辑问题求解系统，经与全球顶尖求解器竞赛测试例对比，我们的求解系统能够解决所有参赛求解器都不能解决的部分问题，其能力达国际先进水平。
3. 一阶逻辑自动推理系统
基于原创的自动推理理论体系，设计了28个一阶逻辑自动推理系统，应用该推理系统已验证来自于程序验证、集成电路验证等实际领域的结论18万余个，解决了一些国际上著名证明器尚未解决的问题；未发现国内其它基于逻辑的动态自动演绎推理系统。
形式化系统研发平台
该平台主要研究形式化相关的理论与方法，形成基于源码、模型以及需求分析方面的形式化技术，并研发相应的形式化工具。
1. 软件需求分析形式化技术
对列车控制、卫星导航、飞行控制等典型系统的软件需求进行形式化分析，形成对应的形式化规格描述、安全性检查规则。
2. 基于源码的形式化技术
对不同编译平台的源程序代码进行预处理及标准化，通过词法分析、语法分析得到结构化的抽象语法树；从语法树中提取控制流并根据程序状态的迁移情况形式化为逻辑公式。工具能够对采用微软CL和GCC编译器编译的C程序源码进行形式化。同时通过预处理技术，也可对PLC、ARM、DSP、C51等系统的嵌入式程序源码进行形式化。
可信性自动验证研发平台
该平台研究基于程序需求或程序源码（如C、PLC等）的快速验证技术以及反例与缺陷定位技术。在形式化系统与自动推理系统基础上研发相应可信性自动验证系统。
1. C程序自动验证技术
采用C程序自动验证技术研发了Scavel C程序自动验证工具。该工具与传统测试工具有本质区别，且通过对比发现，Scavel C能够发现目前市场高占有率的测试工具KlockWork、Testbed等不能发现的缺陷，显现了其独有作用。
基于Scavel C，进一步研发了嵌入式软件可信性自动验证系统。中国工程物理研究院测试中心已将该系统列入其单位技改项目采购计划中，并已上报军委装备发展部。
2. PLC程序自动验证技术
采用PLC程序自动验证技术研发了Scavel PLC 程序自动验证工具。Scavel PLC的性能已达到工业级应用水平，至今未发现其它有效的PLC程序自动验证工具。
基于Scavel PLC，研发了轨道交通控制模块可信性自动验证系统，并对中车唐山机车车辆有限公司的轨道列车网络控制系统实施可信性验证。
3. 基于需求分析的自动验证技术
对软件需求的可信性自动验证，以纠正系统的需求设计缺陷。
