Inferring Invariants by Symbolic Execution
Inferring Invariants by Symbolic Execution
复制标题
通过符号执行推断不变量
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Benjamin Weiß
中科院分区：
文献类型：
--
作者：
P. Schmitt;Benjamin Weiß
在本文中，我们提出了一种推断Java程序中循环不变的方法。整个论文中都使用了一个简单的循环来解释我们的方法。该方法基于符号执行和通过谓词抽象计算固定点的组合。它重复了关键系统Java语义的公理化。该方法已在密钥系统中实现，该系统允许在同一环境中推断不变性并执行验证。我们详细介绍了一个非平凡示例的结果。
In this paper we propose a method for inferring invariants for loops in Java programs. An example of a simple while loop is used throughout the paper to explain our approach. The method is based on a combination of symbolic execution and computing fixed points via predicate abstraction. It reuses the axiomatisation of the Java semantics of the KeY system. The method has been implemented within the KeY system which allows to infer invariants and perform verification within the same environment. We present in detail the results of a non-trivial example.