Efficient Symbolic Simulation of Low Level Software
Efficient Symbolic Simulation of Low Level Software
复制标题
低级软件的高效符号仿真
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Eli Singerman
中科院分区：
文献类型：
--
作者：
T. Arons;E. Elster;S. Ozer;Jonathan Shalev;Eli Singerman
符号执行长期以来一直是形式化硬件验证的主要技术。它在软件中的应用需要处理软件特定复杂性的方法。本文详细阐述了嵌入式软件高效符号模拟的方法;有些方法是新的，有些是对现有方法的改进。使用这些技术，我们已经能够象征性地执行真实的生活微码的数千行，允许正式的方法，成为一个组成部分的微码验证在英特尔公司。
Symbolic execution has long been a staple technique for formal hardware verification. Its application to software requires methods for dealing with software specific complexities. In this paper we elaborate methods for the efficient symbolic simulation of embedded software; some methods are new, others are improvements of existing methods. Using these techniques we have been able to symbolically execute real life microcode of thousands of lines, allowing formal methods to become an integral part of microcode validation in Intel Corporation.