Joogie: from Java through Jimple to Boogie
Joogie: from Java through Jimple to Boogie
复制标题
Joogie：从 Java 到 Jimple 到 Boogie
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Martin Schäf
中科院分区：
文献类型：
--
作者：
Stephan Arlt;P. Rümmer;Martin Schäf
最近，软件验证被用来证明源代码中存在矛盾的存在，从而检测代码中的潜在弱点或为编译器优化提供帮助。与对正确性属性的验证相比，从源代码到逻辑的翻译可以非常简单，因此易于通过自动定理抛弃来解决。在本文中，我们将Java翻译成逻辑，适合证明代码中存在矛盾的存在。我们表明，基于Jimple语言的翻译可用于分析现实世界程序，并讨论Java代码及其字节码之间的差异引起的一些问题。
Recently, software verification is being used to prove the presence of contradictions in source code, and thus detect potential weaknesses in the code or provide assistance to the compiler optimization. Compared to verification of correctness properties, the translation from source code to logic can be very simple and thus easy to solve by automated theorem provers. In this paper, we present a translation of Java into logic that is suitable for proving the presence of contradictions in code. We show that the translation, which is based on the Jimple language, can be used to analyze real-world programs, and discuss some issues that arise from differences between Java code and its bytecode.