IJIT: An API for Boolean Program Analysis with Just-in-Time Translation
IJIT: An API for Boolean Program Analysis with Just-in-Time Translation
复制标题
IJIT：用于布尔程序分析和即时翻译的 API
DOI：
10.1007/978-3-319-66197-1_20
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Wahl, Thomas
中科院分区：
文献类型：
--
作者：
Liu, Peizun;Wahl, Thomas
显式状态转换系统的探索算法是程序验证的核心后端技术。它们可以通过动态生成转换系统应用于程序，避免了昂贵的前期翻译。动态策略需要对实现进行重大修改，将状态直接存储为程序变量的赋值。手动执行的每算法的基础上，这样的修改是费力和容易出错的。在本文中，我们提出了theIjit应用程序编程接口（API），它允许用户自动转换一个给定的过渡系统的探索算法，一个布尔程序上运行。API将系统状态临时转换为程序状态，以便及时通过图像计算向前或向后扩展。使用我们的API，我们毫不费力地扩展了各种非平凡（例如无限状态）的模型检查算法，多线程布尔程序。我们证明了易用的API，并提出了一个案例研究的影响，这些算法的即时翻译。
Exploration algorithms for explicit-state transition systems are a core back-end technology in program verification. They can be applied toprogramsby generating the transition system on the fly, avoiding an expensive up-front translation. An on-the-fly strategy requires significant modifications to the implementation, into a form that stores states directly as valuations of program variables. Performed manually on a per-algorithm basis, such modifications are laborious and error-prone.In this paper we present theIjitApplication Programming Interface (API), which allows users to automatically transform a given transition system exploration algorithm to one that operates onBooleanprograms. The API converts system states temporarily to program statesjust in timefor expansion via image computations, forward or backward. Using our API, we have effortlessly extended various non-trivial (e.g. infinite-state) model checking algorithms to operate on multi-threaded Boolean programs. We demonstrate the ease of use of the API, and present a case study on the impact of the just-in-time translation on these algorithms.
Petri 网和交换半群的指数空间完备问题（初步报告）
DOI：
--
发表时间：
1976
期刊：
Symposium on the Theory of Computing
影响因子：
--
作者：
E. Cardoza;R. Lipton;A. Meyer
通讯作者：
A. Meyer
Boom：布尔程序模型检查更进一步
影响因子：
0.8
作者：
Gérard Basler;M. Hague;D. Kroening;C. Ong;T. Wahl;Haoxian Zhao
通讯作者：
Haoxian Zhao