Java字节码静态资源分析：摊销和分离逻辑结合

可在www.sciencedirect.com在线获取理论计算机科学电子笔记279（1）（2011）19-32www.elsevier.com/locate/entcs基于摊销和分离逻辑的Java字节码静态资源分析Damon Fenacci1 肯尼斯·麦肯齐2爱丁堡大学信息学院英国爱丁堡摘要在本文中，我们描述了一个静态分析器的Java字节码，它使用了摊销分析和分离逻辑的组合，由于罗伯特Atkey。在Java注释的帮助下，我们能够为操作各种基于堆的数据结构的Java方法提供精确的资源利用率约束关键词：Java，JVM，字节码，资源分析，摊销，分离逻辑1引言在[4]中，Robert Atkey展示了如何将摊销复杂性分析的方法与分离逻辑相结合，以获得一种用于操作基于堆的数据结构（如树和链表）的命令式程序的资源分析技术。他展示了如何将这种方法应用于一个小型的基于堆栈的虚拟机，类似于JVM。在本文中，我们描述了一个分析器，它将这种分析应用于真正的JVM字节码，使用从Java源代码中程序员提供的注释中获得的规范纲要我们首先概述分析中涉及的思想。接下来详细描述了用于将规范传达给我们的分析器的Java注释我们还描述了一些在分析器的实现中使用的方法1电子邮件：D. sms.ed.ac.uk2电子邮件：kwxm@inf.ed.ac.uk1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.11.00320D. Fenacci，K.MacKenzie/Electronic Notes in Theoretical Computer Science 279（1）（2011）B致谢本文所述的工作是在爱丁堡大学的RESA项目（EPSRC后续基金资助号EP/G006032/1）中进行的。更多信息可以在[3]中找到。我们感谢Robert Atkey进行了广泛的讨论。2、资源消耗本文的大部分内容都是基于Robert Atkey [4]以前的工作。从非专家的角度来看，这项工作有些技术性，在本节中，我们将尝试给出一个非技术性的概述。我们在这里给出了一个相当简单的例子，但我们希望在RESA网页上提供一个在线演示，包括更复杂的例子。堆行为考虑以下Java代码：class IntList{ int head;IntListtail;IntList concat（IntList p，IntListq）{if（p== null）return q;其他int t = p;while（t.next！=return（t = t.next;t.next= q;return p;}...}}这定义了一个简单的带有整数项的链表类和一个连接两个列表p和q的方法。 如果p为空，则append返回q，否则指针t遍历p直到到达最后一个单元格，然后调整其下一个字段指向q并返回p。假设我们想描述concat的行为。 让我们引入一个断言lseg（a，b），它声明堆中有一个格式良好的列表段，其中a指向第一个单元，b指向最后一个单元。直观地说，在堆中，我们有一个如图1所示的表单，所有单元格都是不同的。个......Fig. 1. 列出段lseg（a，b）。3http://groups.inf.ed.ac.uk/resa/D. Fenacci，K.MacKenzie/Electronic Notes in Theoretical Computer Science 279（1）（2011）21...第一次尝试指定concat方法可能如下所示4：@Requires（lseg（@argp，null），lseg（@arg q，null））//precondition @Ensures（lseg（@ret，null）） //postconditionIntList concat（IntList p，IntList q）{... 个文件夹这个指定的意图是，如果当我们进入方法时，参数p和q指向定义良好的列表段，那么当我们到达方法的末尾时，返回值也将指向定义良好的列表段。规范可以被视为与用户的合同：如果输入该方法满足前提条件，则保证输出满足后置条件。理想情况下，我们将能够证明该方法的实现确实保证了这种行为。不幸的是，上述规范存在一个问题。如果p和q是指向内存中相同位置的指针（换句话说，它们只是同一个列表的不同名称），那么我们最终会得到一个循环结构：我们将沿着p指向的列表的末尾，然后调整下一个指针指向列表的头部：参见图2。Qp图二、在两个指针（p和q）指向同一个列表段的情况下，concat结果这违反了lseg谓词的预期含义，因此后置条件为假。人们可能会尝试通过修改方法来检查p==q，但这仍然不起作用，因为如果p和q指向的列表共享任何单元格，我们仍然会得到包含循环的堆结构（图3）。修改方法来检测这种情况将使它不必要地p图3.第三章。在指针q指向由p指向的列表段的内部元素的情况下，concat结果。更好的策略是修改断言，从一开始就排除有问题的输入。其中的关键是将断言建立在分离逻辑[22]的基础上，分离逻辑是一种设计用于讨论非重叠结构的逻辑，近年来在分析堆分配的数据结构时被证明非常有用。分离逻辑有许多新颖的逻辑连接词，用于讨论非重叠对象。例如，除了通常的逻辑合取4为了清晰起见，我们在这里使用了理想化的注释语法。对Java注释语法的限制意味着实际中使用的规范要复杂一些;下面将对这些规范进行描述在第3节中详细介绍。Q...22D. Fenacci，K.MacKenzie/Electronic Notes in Theoretical Computer Science 279（1）（2011）（A在堆分配结构的上下文中，A和B将被解释为意味着A和B都为真，但是在堆的不相交区域上。参见[22]，了解分离逻辑的全部细节如果我们使用分隔连词将原始的规范重写为@Requires（lseg（@arg p，null）* lseg（@arg q，null））@Ensures（lseg（@ret，null））则它变为有效：如果用户提供不共享存储单元的两个格式良好的列表，则返回值也是格式良好的列表。使用分离逻辑进行上一节的技术允许我们指定操作堆分配结构的方法的函数属性。然而，我们的主要兴趣是方法的资源消耗，其中在本文中，我们将考虑确定一个名为consume的特殊方法的执行次数的问题，但这可以很容易地被其他方法或字节码指令所取代，以便处理其他资源。在[4]中，它表明分离逻辑中的断言可以巧妙地扩展到包括有关资源消耗的信息，并且可以验证注释并推断方法的资源使用情况，其中迭代由堆分配的数据结构的处理这是基于涉及数据结构的算法的摊销分析[25]的想法这里我们将采用的方法是假设数据结构的每个节点都配备了许多令牌，并且每次处理节点时都会消耗其中一个令牌。考虑我们前面的例子，添加了一些消费调用：IntList concat（IntList p，IntList q）{ consume（）;return（）;if（p==null）return q;else {int t = p;while（t.next！=publicintt.nextfindDuplicate（）;}t.next= q;return p;}我们看到consume在方法开始时被调用两次，然后为列表p中的每个节点调用一次。我们可以通过扩展我们的分离逻辑规格来表达这一点，以包括成本：@Requires（lseg（1， @argp，null） *lseg（0，@argq，null）， 2）@Ensures（lseg（0， @ret，null），0）D. Fenacci，K.MacKenzie/Electronic Notes in Theoretical Computer Science 279（1）（2011）23额外的数字注释被解释为，如果我们为p的每个节点输入一个token加上两个额外的token，那么方法可以成功执行，并且在最后我们没有任何token;由于每个调用consume需要一个token，我们看到consume最多被调用长度（p）+2次。我们不要求注释指定所需的最小标记数，只需要一个足以让方法完成的标记数。例如@Requires（lseg（7， @argp，null） *lseg（2，@argq，null）， 5）也是一个有效的前提条件：如果我们有指定数量的令牌，那么该方法仍然能够完成，但这次我们将剩下一些令牌剩余的标记可以包含在后置条件中。例如@Requires（lseg（7， @argp，null） *lseg（2，@argq，null）， 5）@Ensures（lseg（2， @ret，null），3）也是一个有效的（尽管不是最佳的）规范。Atkey表明，可以使用基于Hofmann和Jost [15]思想的线性规划技术来验证上述资源注释是否有效;事实上，他表明实际上可以推断出最小资源注释，从而推断出方法的资源消耗。我们稍后会看到这方面的例子。3Java字节码我们已经开发了一个分析器，它实现了前一节的思想源程序配备了Java注释，给出了上述类型的前置条件和后置条件;当前版本还需要给出循环不变式的注释。我们的分析器在编译的类文件上工作。Java编译器将源代码注释存储在类文件中，分析器检索这些注释并使用它们对JVM字节码执行分析分析字节码而不是源代码的技术有几个优点：• 字节码是实际执行的代码。我们不需要任何特定编译器内部工作的知识，实际上分析器是独立于所使用的编译器的。• 这种方法扩展了JVM验证范例。许多Java应用程序都是以编译后的类文件的形式提供的，没有源代码，字节码分析器可以用来在执行之前检查类的行为。没有要求代码的用户信任供应商。• 分析并不局限于从Java源代码获得的字节码;原则上，我们的分析可以对从其他语言获得的字节码起作用24D. Fenacci，K.MacKenzie/Electronic Notes in Theoretical Computer Science 279（1）（2011）assertions =[exvars] assertion（'||' assertion）* ;assertion = '{' data-assertions '|'堆断言|'resource-assertion'}';exvars=;typedvar=id（* id是Java标识符：[A-Za-z_][A-Za-z 0 -9_]* *）type = 'int'|'长'|'浮动'|“双”|'ref';data-assertion= data-assertionterm| term ’!=’术语;heap-assertions= heap-assertion’[’| ’lseg (’ resource-assertion ’,’ term ’,’ term ’)’| ’tree (’ resource-assertion ’,’ term ’)’;term =id（* existential variable *）| ’@arg’ id (* only @arg variables allowed in preconditions *)|’@var’ id|'空'| '@ret';（*@ret只允许在后置条件中使用 *）field= id '：' type ; location=var|“是吗？”;resource-assertion= linear-expression;见图4。 断言EBNF针对JVM（例如Scala5），甚至是手写字节码。用于摊销分析我们使用Java注释来为方法提供资源使用规范。在本节中，我们将扩展前面几节中给出的非正式描述Java注解是一种特殊形式的元数据，可以添加到Java源代码中。它们可以与Java类，字段，方法和方法参数相关联，并在编译Java代码时嵌入类文件中。它们是使用以注释命名的文件中的类结构为了能够提供方法的摊销分析，我们定义了三个注释。这些允许用户指定方法的先决条件和后置条件以及分析器所需的循环不变式• @Requires（断言）先决条件• @确保（断言）后置条件• @Invariant（assertions）用于循环不变式所有这些都以包含断言的JavaString的形式给出EBNF中断言语法的缩短版本如图所示四、数据断言由逗号分隔的断言列表组成，==term or term！= 术语和用于向分析仪提供信息5http://www.scala-lang.org/D. Fenacci，K.MacKenzie/Electronic Notes in Theoretical Computer Science 279（1）（2011）25关于引用何时指向相同或不同的Java对象。这些在循环不变量中是必需的。使用数据流分析来推断这些信息是可能的，但我们还没有这样做。有两种类型的堆断言，它们是富含字段内容指示的分离逻辑谓词。堆断言的第一种类型表明堆的这一部分形成列表段或树（例如lseg（r1，@argx，null），tree（r1，@arg x））;这两个都扩展到从分离逻辑原语构建的更复杂的断言。第二种类型的堆断言表明，分析器，一个特定的字段指向一个特定的堆位置或一些不确定的位置;这些主要是在前置条件和后置条件中需要的，它们通过暴露有关堆结构的信息来促进过程间分析，用于分离逻辑的推理最后，资源断言是线性表达式，如3*r1+5*r2+r3+ 7指定了我们希望分析器使用的常量和变量，在执行之前和之后（即在前置条件和后置条件中）推断与方法相关的资源;它们也用于列表和树谓词中，以指示与结构的每个节点相关的资源我们还引入了一个名为consume的虚拟方法，它除了告诉静态分析器，在它被引入的地方，资源正在使用。我们可以想象这样一个虚拟方法在未来隐藏在库代码中，说明每个类中定义的每个方法所使用的资源量，这样程序员就不需要显式添加它，而是通过调用库方法隐式使用它。然而，在目前的实现中，库还没有被修改，开发人员必须在代码中显式地指定资源消耗。Java代码中的不变量本地化为了使摊销分析有效，必须为每个循环提供循环不变量，但Java语言不允许在代码中包含注释如果被分析的方法包含两个或多个循环，这是有问题的，因为我们需要一种方法来决定哪个不变量引用哪个循环。我们可以简单地按照循环在代码中出现的顺序给出不变量，但是编译器可能会产生这样的字节码，其中循环在字节码中出现的顺序我们克服这个限制的方法是用一个整数标识符来标识每个循环。每个循环不变式都有一个标识符（@Invariant（id，assertion）），同一个标识符必须匹配一个伪方法Loop.invariant（id）的参数，该方法放置在代码中循环之前。因此，通过搜索代码，分析器可以将声明的不变量与相应的循环相关联。4示例和输出解释我们通过回到前面的列表关联示例来说明分析器的操作。26D. Fenacci，K.MacKenzie/Electronic Notes in Theoretical Computer Science 279（1）（2011）$ cat examples/IntList.javaimportuk.ac.ed.inf.resa.*;public class IntList {private int data;private IntList next;...@Requires（“{|lseg（1，@arg p，null）* lseg（0，@arg q，null）|”）@Ensures（“{|lseg（0，@ret，null）|0}”）@Invariant（“{@vart！= null |lseg（0，@var p，@vart）*”+ “lseg（1，@var t，null）* lseg（0，@var q，null）|public static int findDuplicate（int findDuplicate）{Amortized.consume（）;Amortized.consume（）;if（p==null）return q;IntList t = p;Loop.invariant（0）;while（t.next！=空值）{t=t.next;return（）;}t.next= q;return p;}...}我们提供了一个循环不变量，它描述了程序进行时资源使用的状态当我们到达while循环的头部时，我们已经用完了与第一个输入列表p中已经处理过的部分（在p和t之间）相关的资源，我们在p的剩余部分（在t和null之间）仍然有一个可用的资源单元，并且我们不需要任何资源来处理q。请注意附加到变量名的@arg和@var注释。它们用于区分变量的当前值（@var）和方法入口处的方法参数值（@arg）;它们在本例中不是严格必需的，但在更复杂的示例中是必需的，其中修改了表示方法参数的变量。@ret注释引用方法返回值。如果我们编译IntList.java并调用分析器，则输出如下。$ resa -amounted examples/IntList concat...解决VC验证成功这表明分析者已经成功地证明了先决条件和后置条件是满足的。但是，如果我们修改前提条件，@Requires（“{|lseg（1，@arg p，null）* lseg（0，@arg q，null）|1}”）那么验证失败，因为只有一个LP不可行更有趣的是，我们可以提供通用的注释，分析器将为它们推断合适的值。@Requires（“{|lseg（x1，@arg p，null）* lseg（x2，@argq，null）|”）@Ensures（“{|lseg（y1，@ret，null）|y2}”）@Invariant（“{@vart！= null |lseg（z1，@var p，@vart）*”+ “lseg（z2，@var t，null）* lseg（z3，@var q，null）|z 4 }”）D. Fenacci，K.MacKenzie/Electronic Notes in Theoretical Computer Science 279（1）（2011）27通过这些注释，分析器输出资源变量的最佳解决方案：x1 =1，x2 =0，x3 = 2y1 =0，y2 = 0z1 =0，z2 =1，z3 =0，z4 = 0我们还可以指定方法返回时所需的资源量：如果我们将后置条件替换为@Ensures（“{|lseg（3，@ret，null）| 7}") then we get x1 = 4, x2 = 3, x3 = 9, so that if the postcondition is to如果满足，那么我们必须为p的每个元素提供4个单元的资源，为q的每个元素提供3个单元的资源，并且在调用该方法之前需要9个额外的单元除了这个例子之外，我们还成功地分析了列表上的其他一些标准操作，例如反转、迭代、删除和插入元素，以及树的类似操作5实现细节我们的分析器是用OCaml实现的，Java类文件由一组数据库表示。对于程序分析，最重要的部分是方法字节码的表示。我们的设计是相当通用的，因为我们打算支持多种分析技术，包括前面描述的Java类文件最初被转换为低级OCaml表示，这是JVM规范中描述的类结构的相当忠实的表示[19]。然后将其转换为更适合分析的更高级别的表示。我们将在这里给出这种表示的概要，但是空间限制排除了详细描述。字节码指令被反编译成一种消除了JVM堆栈的形式。我们跟踪哪些常量和局部变量被加载到堆栈上，这些变量由一个名为value的数据类型表示，类型为int、long、float、double、String和class的常量的构造函数，以及变量。变量由整数标识符表示，这些标识符标记有相应值的类型：这是I，L，F，D或A之一（表示整数，长整数，双精度数和地址）。对于boolean、byte、char和short，我们没有特殊的类型，因为JVM在大多数情况下都将它们视为32位整数我们还用单个类型A标记所有引用，并且不试图跟踪最具体的类或接口 变量所属的变量;可以推断出这些信息，但到目前为止我们还没有要求。变量有两种：局部变量和堆栈变量。for- mer表示通过指令（如iload）从JVM局部变量加载到堆栈上的值，后者表示通过算术运算、方法调用等在堆栈上创建的中间值。每个变量都标记有一个整数，对于局部变量，该整数表示相关JVM局部变量的编号，对于堆栈变量，该整数只是一个计数器，每当在堆栈上创建新值时递增，然后递减28D. Fenacci，K.MacKenzie/Electronic Notes in Theoretical Computer Science 279（1）（2011）当这个值被消耗的时候。这里需要注意，因为堆栈操作可能会复制堆栈上的值。反编译过程通过使用称为Copy的特殊伪指令创建变量的新副本来处理此问题。另一个复杂性是，可以将局部变量r加载到堆栈上，然后在较早的值（仍然在堆栈上）被消耗之前修改r的内容;同样，复制操作用于通过创建表示较早的值作用于堆栈的指令由以值作为参数的操作的数据类型表示。它有19个构造函数，它们代表了所有的JVM操作（putfield、getfield、invokevirtual等等），除了那些涉及控制流传输的操作。基本块由一个对列表表示，这些对由操作以及存储操作结果（如果有的话）的局部变量或堆栈位置组成。在一个基本块的末尾，我们有一个延续数据类型的成员：这代表了各种类型的跳转、比较、切换和返回操作，以及指定控制在离开当前块后可以跳转到哪些块的信息。我们不提供异常处理程序使用的jsr和ret指令的任何表示，因为这些指令使分析复杂化，并且在当前的Java版本中被认为是不推荐的（尽管我们在rt.jar中的一些标准API类中遇到过它们）。如果在反编译期间遇到这些指令之一，则抛出异常并拒绝该类整个方法的字节码由一个块数组表示，按前序存储这可以被看作是一个图，我们有一个模块，它可以计算有用的信息，如后继者，前导者和支配者，也可以提供图的其他视图，如后序和反向后序，这在某些分析中可能是有用的证明搜索摊销分析最重要的部分是证明搜索过程，用于验证方法的前提条件是否包含其后置条件，以及检查或推断相关的资源注释。这使用了Atkey在[4]中描述的方法，实际上，我们的实现使用了Atkey原型实现的代码改编版本，该原型实现分析了JVM字节码子集的文本形式。基本思想是访问后序中的代码，从后置条件向后工作，以推断每个指令的最弱前置条件，然后证明第一个指令的最弱前置条件在后序中访问CFG的节点可以确保当我们访问给定的节点n，其所有后继的前置条件都是已知的，因此可以组合（通过逻辑合取）以获得n的后置条件。但这当我们遇到一个后沿s→t（即，当t在一个循环）。在这种情况下，当我们到达s时，我们还没有访问过t，正是由于这个原因，我们需要循环不变式的注释：注释将为t提供一个前提条件，因此将有助于后置条件D. Fenacci，K.MacKenzie/Electronic Notes in Theoretical Computer Science 279（1）（2011）29对于t。证明搜索过程还收集描述字节码指令的资源使用的线性约束，如[ 4 ]中所述;一旦分析已经完成，并且已经检查了基本的分离逻辑注释，以确保前提条件暗示了后置条件，资源约束就被转换成线性规划问题，然后使用帕尔马多面体库[5]来求解该线性规划问题。6结论和进一步研究我们已经表明，它是可能的应用Atkey的摊销分析技术，以现实的JVM字节码。然而，有一些问题值得进一步研究。• 注释有些复杂，希望简化它们。第一步是免除数据相等和不相等注释，我们相信使用数据流技术可以做到这一点。一个更困难的问题是删除循环不变式，这通常是规范中最困难的部分。已经研究了自动推断循环不变量的技术，并且这里使用的这种循环不变量的一种可能的攻击途径是[10]中描述的方法• 一个小小的不便是断言语法只在分析期间检查，而不是在编译时。Sunjavac编译器支持- notation processing6的插件，在编译期间使用此特性来检测断言语法中的• 摊销技术对于分析处理堆分配结构的循环的资源消耗是有用的，但对于由数字量控制我们的分析器可以通过使用组合技术来枚举多面体中的格点来攻击这样的循环（参见[6]和[9]相关技术在Java程序资源分析中的应用）;[3]中对此进行了初步描述，我们将在后续论文中给出更多细节。一个有趣的问题将是自动结合这两种技术，使分析器可以处理复杂的方法，从用户的干预最小• 摊销分析只能处理在所涉及的数据结构的大小上是线性的资源使用的界限其他作者的经验[8]表明，这在许多（但绝不是所有）实际情况下是足够的。我们在这里使用的基于线性规划的推理技术本质上与线性边界有关;然而，最近的工作[14，13]已经展示了如何在某些特殊情况下扩展到推导非线性边界。还有其他的推理技术可以处理非线性边界，我们将在后面讨论其中的一些。6参见JSR 269：Pluggable Annotation Processing API。30D. Fenacci，K.MacKenzie/Electronic Notes in Theoretical Computer Science 279（1）（2011）• 分析器目前只支持链表和树，证明搜索的实现非常依赖于此。希望找到更通用的注释和分析技术，例如用于处理通过接口访问的标准Java API中的数据结构。这里的一种方法可能是将注释附加到现有的库类，以便能够分析客户机代码。相关工作：资源推断近年来，关于资源推断的工作已经相当多，我们现在试图描述其中的一些这里使用的基于线性编程的推理技术起源于Hofmann和Jost [15]，随后被应用于OCaml风格的语言[23]和用于嵌入式系统的Hume语言[8]。Jost最近的一些发展出现在[14，13]。许多其他的资源推理技术已经被提出和实现，用于Java和其他语言。 Albert et的COSTA系统 [1，2]将JVM字节码转换为一组与我们的方法相比，COSTA是全自动的，不需要用户提供注释。Gulwani等人的SPEED项目[11，12]使用了许多技术（包括抽象解释和SMT求解）来获得程序位置被访问次数的（非线性和符号）界限，并已应用于C#程序的复杂性分析资源使用推断的类型理论方法在[21]（递归函数程序的符号边界的推断）和[20]（面向对象程序的堆使用）中描述相关工作：字节码在文献中已经出现了许多JVM字节码的表示。其中许多（例如[18]，[7]和[2]）利用引入新变量的技术来表示JVM操作数堆栈上的值。Soot框架（例如，参见[26]）包含了许多JVM字节码的中间表示，并已被应用于优化和分析中的许多问题;相关出版物的列表可以在www.example.com上http://www.sable.mcgill.ca/。JVM字节码分析的另一个框架是Julia，在[24]中描述。最后，JVM类文件的另一种OCaml表示在[16]中描述;这与我们的表示有很多共同之处D. Fenacci，K.MacKenzie/Electronic Notes in Theoretical Computer Science 279（1）（2011）31引用[1] 埃尔维拉·阿尔贝特，普里·阿雷纳斯，萨米尔·杰纳伊姆，热尔姆·安·普埃布拉和达米亚诺·扎纳尔迪尼。Java字节码的成本分析Rocco De Nicola，编辑，第16届欧洲编程研讨会，ESOPSpringer-Verlag，2007年3月[2] 埃尔韦拉·阿尔伯特，普里·阿里纳斯，萨米尔·杰奈姆，热尔姆·安· 普埃布拉和达米亚诺· 扎纳尔迪尼。COS TA：Java 字 节 码 开 销 和 终 止 分 析 器 的 设 计 和 实 现 。 在 Formal Methods for Components andObjects，第六届国际研讨会，FMCO 2007，阿姆斯特丹，荷兰，2007年10月24-26日，修订的讲座，计算机科学讲座笔记第5382卷，第113-132页。Springer，2008.[3] David Aspinall，Robert Atkey，Kenneth MacKenzie，and Donald Sannella. Java字节码资源分析的符号和分析技术。第五届Trustworthly Global Computing，TGC'10，第1-22页，柏林，海德堡，2010年史普林格出版社[4] 罗伯特·阿特基基于分离逻辑的摊销资源分析 见ESOP，第85[5] R.巴尼亚拉，P.M. Hill和E.再见帕尔马多面体库：为硬件和软件系统的分析和验证提供一套完整的数值抽象。Science of Computer Programming，72（1[6] 作者：Alexander Barvinok，James E.波莫斯海姆 多面体格点的算法理论。在代数组合学的新观点（伯克利，加利福尼亚州，1996年至1997年），数学卷38。Sci. Res. Inst. Publ. 第91剑桥大学出版社，剑桥，1999年。[7] 伦纳特·贝林格肯尼斯·麦肯齐伊恩·斯塔克Grail：一种用于命令式移动代码的函数形式。在全球计算基础：第二届EATCS研讨会论文集，在理论计算机科学电子笔记中的第85.1Elsevier，2003年6月[8] Armelle Bonenfant，Christian Ferdinand，Kevin Hammond，and Reinhold Heckmann.纯函数式语言的最坏情况执行时间。函数式语言的实现（IFL 2006），计算机科学讲义第4449卷，2007年。出现。[9] 维克多·布拉伯曼，迭戈·加伯韦茨基，塞尔吉奥·尤文。一种静态分析，用于合成动态内存消耗的参数规格。Journal of Object Technology，5（5）：31[10] 放大图片作者：Peter W.奥赫恩和杨洪锡用双外展法进行组合形状分析在POPL，第289[11] 作者：Sumit Gulwani Mehra和Trishul M.奇林比SPEED：对程序计算复杂性的精确和高效的静态估计。在POPL，第127[12] 苏米特·古尔瓦尼和弗洛里安·祖莱格可达性约束问题。在2010年ACM SIGPLAN编程语言设计和实现会议中，PLDIACM。[13] 杨·霍·霍夫曼、克劳斯·艾利格和马丁·霍夫曼。多元摊销资源分析。 在第38届研讨会关于Prog.兰斯(POPL'11），2011年。出现。[14] 杨·霍·霍夫曼和马丁·霍夫曼。具有多项式势的资源分摊分析-函数程序多项式边界的静态推断在第19届欧洲编程研讨会（ESOP'10）的会议记录中Springer，2010.[15] Martin Hofmann和Ste Escheren Jost。一阶函数式程序堆空间使用的静态预测。在POPL，第185-197页[16] Laure ntHu bert ， NicolasBar r'e ， Fr'e d'ericBesson ， DelphineDemange ， ThomasP. Jensen ， VincentMonfort ， David Pichardie ， and Tophaine Turpin. Sawja ： Java 静 态 分 析 研 讨 会 。 CoRR ，abs/1007.3353，2010年。[17] Ste EscherenJost. 尸体解剖和分析。 博士论文，路德维希-马克西米利安大学，慕尼黑，2010年8月。[18] Christopher League，Valery Trifonov，and Zhong Shao. 函数式Java字节码。 第五届世界系统学、控制论和信息学大会论文集，2001年7月。Java虚拟机的中间表示工程[19] 蒂姆·林德霍尔姆和弗兰克·耶林。Java虚拟机规范。爱迪生-韦斯利·朗曼出版公司股份有限公司、美国马萨诸塞州波士顿，第2版，1999年。[20] Wei ngan Chin，Huu Hai Nguyen，Shengchao Qin，and Martin Rinard. 内存使用验证oo程序。在SAS 05中，第70Springer，2005.32D. Fenacci，K.MacKenzie/Electronic Notes in Theoretical Computer Science 279（1）（2011）[21] A'l varoJ. 关于Portillo，KevinHammond，Hans-W olfgangLoidl和PedroVasconcelos。使用自动大小和时间推断进行成本分析。第14届函数式语言实现国际会议论文集，IFL'02，第232-247页，柏林，海德堡，2003年。施普林格出版社。[22] John C.雷诺兹分离逻辑：共享可变数据结构的逻辑。2002年，第17届IEEE计算机科学。[23] Donald Sannella、Martin Hofmann、David Aspinall、Stephen Gilmore、Ian Stark、Lennart Beringer、Hans-Wolfgang Loidl、Kenneth MacKenzie、Alberto Momigliano和Olha Shkaravska。 流动资源保障（项目评价文件）。函数式编程的趋势，第211-226页，2005年。[24] 福斯托·斯波托JULIA：Java字节码的通用静态分析器。《2005年FTfjP会议记录》[25] 罗伯特·恩德雷·塔扬。分摊计算复杂度。SIAM Journal on Algebras and Discrete Methods，6（2）：306[26] RajaVall'ee-Rai ， LaurieHenrique ， VijaySundaresan ， PatrickLam ， EtienneGagnon ，andPhongCo.Soot-a Java optimization framework. 在CASCON 1999的Proceedings，第125