CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic - (Competition Contribution)
CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic - (Competition Contribution)
复制标题
支持递归程序和浮点运算的 CPAchecker -（竞赛贡献）
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Philipp Wendler
中科院分区：
文献类型：
--
作者：
Matthias Dangl;Stefan Löwe;Philipp Wendler
我们向SV-COMP'15提交了软件验证框架CPAchecker。提交的配置是七种不同分析的组合，基于显式值分析，k-归纳，谓词分析和具体的内存图。这些分析使用的概念，如CEGAR，懒惰抽象，插值，可调块编码，有界模型检查，不变式生成，和块抽象记忆。找到的反例通过位精确分析进行交叉检查。几种不同分析的组合很好地应对了SV-COMP中验证任务的多样性。
We submit to SV-COMP'15 the software-verification framework CPAchecker. The submitted configuration is a combination of seven different analyses, based on explicit-value analysis, k-induction, predicate analysis, and concrete memory graphs. These analyses use concepts such as CEGAR, lazy abstraction, interpolation, adjustable-block encoding, bounded model checking, invariant generation, and block-abstraction memoization. Found counterexamples are cross-checked by a bit-precise analysis. The combination of several different analyses copes well with the diversity of the verification tasks in SV-COMP.