Embedded Software Verification Using Symbolic Execution and Uninterpreted Functions
Embedded Software Verification Using Symbolic Execution and Uninterpreted Functions
复制标题
使用符号执行和未解释函数的嵌入式软件验证
DOI：
10.1007/s10766-005-0004-8
复制
发表时间：
2006
影响因子：
1.5
通讯作者：
S. Rajan
中科院分区：
文献类型：
--
作者：
David W. Currie;Xiushan Feng;M. Fujita;Alan J. Hu;Mark Kwan;S. Rajan
符号模拟和未解释函数一直是形式化硬件验证的主要技术。近年来，我们已经适应了这些技术的自动化，正式验证低层次的嵌入式软件，具体来说，检查等价的汇编语言程序的不同版本。我们的方法，虽然有限的可扩展性，已被证明是特别有前途的复杂的代码优化和复杂的体系结构典型的高性能嵌入式软件，如DSP和VLIW处理器。事实上，我们的一个关键发现是，创建或重新定位我们的验证工具以适应不同甚至非常复杂的机器是多么容易。由此产生的工具自动验证或发现以前未知的错误，在几个小序列的工业和发布的示例代码。本文介绍了这些技术和审查我们的结果。
Symbolic simulation and uninterpreted functions have long been staple techniques for formal hardware verification. In recent years, we have adapted these techniques for the automatic, formal verification of low-level embedded software—specifically, checking the equivalence of different versions of assembly language programs. Our approach, though limited in scalability, has proven particularly promising for the intricate code optimizations and complex architectures typical of high-performance embedded software, such as for DSPs and VLIW processors. Indeed, one of our key findings was how easy it was to create or retarget our verification tools to different, even very complex, machines. The resulting tools automatically verified or found previously unknown bugs in several small sequences of industrial and published example code. This paper provides an introduction to these techniques and a review of our results.