Applying SMT in symbolic execution of microcode

Applying SMT in symbolic execution of microcode
复制标题

SMT在微码符号执行中的应用

DOI：
--
复制
发表时间：
2010
期刊：
Formal Methods in Computer-Aided Design
影响因子：
--
通讯作者：
Jonathan Shalev
Jonathan Shalev
中科院分区：
--
文献类型：
--
作者：
Anders Franzén;A. Cimatti;Alexander Nadel;R. Sebastiani;Jonathan Shalev

文献摘要

被引文献

相似文献

微代码是现代微处理器中的一个关键部件，在过去已经投入了大量的努力来验证其正确性。一个突出的方法，基于符号执行，传统上依赖于使用布尔SAT求解器作为后端引擎。本文研究了可满足性模理论（SMT）在微码验证问题中的应用。我们整合MathSAT，SMT求解器的位向量理论，在微码验证的流程，并通过实验评估一些优化的有效性。结果表明，SMT技术的潜力超过纯布尔SAT。
Microcode is a critical component in modern microprocessors, and substantial effort has been devoted in the past to verify its correctness. A prominent approach, based on symbolic execution, traditionally relies on the use of boolean SAT solvers as a backend engine. In this paper, we investigate the application of Satisfiability Modulo Theories (SMT) to the problem of microcode verification. We integrate MathSAT, an SMT solver for the theory of Bit Vectors, within the flow of microcode verification, and experimentally evaluate the effectiveness of some optimizations. The results demonstrate the potential of SMT technologies over pure boolean SAT.