技术详细介绍
Scavel 程序可信性验证工具是西南交通大学联合多个单位研发的以自动推理为核心技术的程序可信性自动验证工具，验证对象为可信性、可靠性要求高的安全关键软件。
Scavel C 工具提供C语言程序中包括数组越界、被零除、指针无效、内存泄漏、数据溢出、数值无效等多种缺陷类型的验证功能（现有静态分析工具大多交叉覆盖2～3项），还可验证其他与程序变量有关的自定义性质。
Scavel PLC工具提供PLC程序中数组越界、被零除、数据溢出等多种缺陷类型的验证，还可检测程序是否符合IEC61131-3标准规范。
应用领域：Scavel 程序可信性验证工具面向航空航天、国防军工、卫星导航、轨道交通等重要领域，为运行与这些领域的高可信性安全关键软件提供验证服务。到目前为止，Scavel 程序可信性自动验证工具已服务了20多个单位，完成了160多万行经过严格测试的C程序、20万行PLC程序源码的验证，验证出问题点300多处，致命问题点数十处。
知识产权情况：核心技术申报国家发明专利13项，相关软件取得计算机软件著作权登记证书6项。
技术水平：国际先进。
技术成熟度：熟化阶段，已为涉及航空航天、国防军工、卫星导航、轨道交通、信息电子等领域的多个单位提供了验证服务，其效果显现了Scavel验证工具的独有能力。
团队简介：系统可信性自动验证国家地方联合工程实验室于2016年10月获国家发改委批准建设，西南交通大学为建设单位。实验室围绕高安全软件可靠性检测的重大需求，以原创的自动推理体系为核心支撑，借鉴并发展了国际上先进的形式化技术，致力于科学有效的系统可信性自动验证技术及工具的研发，以摆脱系统可信性自动验证技术对国外的依赖，提高我国在可信性验证领域的自主创新能力，为系统的可信运行提供科学、有力保障。