一、简介

      Scavel C 工具(简称)，是系统可信性自动验证国家地方联合工程实验室在系统可信性验证相关理论与技术方面积累大量原创性研究成果的基础上,开发的以形式化和自动推理为核心技术的自主可控工具。

二、功能

      (1)验证C语言程序中的数组越界、内存泄漏、指针安全、数据溢出、除数为零、非数字和代码可达性，提供存在问题或不存在问题的验证结果；

      (2)验证C语言中与程序变量或表达式有关的自定义性质，如用户指定的表达式是否成立等，提供存在问题或不存在问题的验证结果。

三、特点

      在不修改、不运行源程序的情况下，以静态方式验证程序运行时错误(Run-Time Errors)，对比基于静态分析的测试工具其优势是源代码中的变量动态变化,对比动态测试工具的优势是不需要搭建测试环境、运行源码和构建测试例，并保证遍历所有可能执行路径以证明源代码的正确性。