IJIT：基于即时翻译的布尔程序分析 API（扩展技术报告）
软件工程
2017-06-13 v1
摘要
显式状态迁移系统的探索算法是程序验证中的核心后端技术。通过即时生成迁移系统可将其应用于程序，从而避免高昂的前期翻译开销。即时策略需要对实现进行重大修改，使其成为直接将状态存储为程序变量赋值的形式。基于每个算法手动执行此类修改既费时又容易出错。本文提出了 IJIT 应用程序编程接口 (API)，允许用户将给定的迁移系统探索算法自动转换为操作于布尔程序的算法。该 API 在进行前向或后向图像计算展开之前，将系统状态临时转换为程序状态。利用我们的 API，我们轻松地将各种非平凡（如无限状态）模型检测算法扩展至多线程布尔程序上运行。我们展示了该 API 的易用性，并给出了关于即时翻译对这些算法影响的案例研究。
引用
@article{arxiv.1706.03167,
title = {IJIT: An API for Boolean Program Analysis with Just-in-Time Translation (Extended Technical Report)},
author = {Peizun Liu and Thomas Wahl},
journal= {arXiv preprint arXiv:1706.03167},
year = {2017}
}
备注
The 15th International Conference on Software Engineering and Formal Methods (SEFM 2017)