使用逻辑分析和转换验证Java字节码
摘要：将LP范式中最先进的分析器转移到Java字节码（JVML）的分析和验证，以自动传播LP分析工具的能力。我们依赖于元编程和程序特化的众所周知的技术来实现我们的目标。更具体地说，我们建议部分评估在LP中实现的JVML解释器以及（JVML程序的LP表示），然后分析剩余程序。有趣的是，至少对于我们所研究的示例，我们的方法产生的原始JVML程序的LP表示非常简单。这可以看作是从JVML到高级LP源码的反编译。通过对这样的剩余程序进行推理，我们可以在CiaoPP系统中自动证明JVML程序的一些非平凡属性，如终止性，运行时错误的自由性，并推断其资源消耗的界限。我们不知道还有哪个系统能够验证Java字节码的这些高级属性。
作者：Elvira Albert, Miguel G''omez-Zamalloa, Laurent Hubert, German Puebla
论文ID：1007.3250
分类：Programming Languages
分类简称：cs.PL
提交时间：2010-11-22