DFS引擎采用LLVM IR作为目标程序的表示方式,利用深度优先搜索(DFS)算法遍历目标程序的状态空间,并调用约束求解器判断该目标程序是否满足待验证属性。

Ceagle默认采用DFS引擎进行验证,若要显式指定其使用DFS引擎,用法如下:

  • 网页版
    • // 网页版用法
  • 命令行版
    • ceagle --engine=dfs example.c
    • 详细使用方法请参阅验证引擎参数。

在此基础上,针对大型目标程序(或状态空间太大的目标程序),Ceagle提供以下技术提高验证效率:

  • 抽象精化
  • 组合验证