诚
这篇论文介绍了一个名为Serval的框架，用于通过符号执行来对系统代码进行可扩展的自动化验证。
Serval的核心思想是将开发人员使用Rosette编写指令集解释器并转化为自动化验证器，从而实现系统软件的验证。这一框架通过符号性能分析和优化来识别和修复验证性能瓶颈。作者通过将Serval应用于现有的系统和未经验证的系统中，展示了其在找到系统错误和提高验证效率方面的有效性。
