MMJul, 2019

由 (条件) 终止证明驱动的资源分析

PDF
TL;DR该论文提出了一种资源分析方法，它使用终止分析结果驱动成本关系系统（CRS）的生成，并且最终生成的线性有界 CRS（LB-CRS）克服了现有技术产生复杂程序流程的成本函数难以解决的问题，作者还制定了一种名为 MaxCore 的资源分析工具，并针对 C 整数程序的一组基准测试进行了实验，结果显示 MaxCore 优于其他所有资源分析工具。
resource analysiscomplex control flowtermination analysislinearly-bounded crsmaxcore
发现论文，激发创造
  • 使用线性约束进行逻辑编程的终止分析

    这篇论文提出了规则受限和循环受限程序的新类别，通过更全局地分析术语如何从规则的主体传播到头部来克服目前方法的各种限制。

    Dec, 2015

  • 一种基于机器学习的解决递归关系的方法及其在逻辑程序成本分析中的应用

    用于计算程序资源使用情况的自动静态成本分析方法，基于回归关系解决递归方程求解问题，结合机器学习回归技术、SMT 求解器和计算代数系统，提出了一种新的、通用的方法来解决任意受限递归关系方程，证明在 CiaoPP 系统中能够胜过现有最先进成本分析工具和递归求解器，并解决不能被它们解决的递归方程。

    May, 2024

  • 通过术语重写自动终止逻辑程序的证明

    本文介绍了通过改良变换法来解决逻辑程序终止性分析的限制的方法，并将其应用于 AProVE 终止证明器进行实验与评估。

    Mar, 2008

  • 使用机器学习解决递归关系，并应用于成本分析

    开发了一种利用机器学习稀疏回归技术猜测候选闭合形式函数并使用 SMT 求解器和计算机代数系统来验证是否是递归关系的解的新型通用方法，相比传统方法在给定时间内能够找到一类不能被现有分析系统或当前计算机代数系统解决的递归式的闭合解。

    Aug, 2023

  • 通过部分求值进行控制流细化及其在终止和成本分析中的应用

    本文旨在研究使用 Horn 子句的部分求值作为整数转换系统控制流细化的通用技术，借助该技术可以证明循环程序的终止性和复杂度等性质，提高程序分析的精度。

    Jul, 2019

  • 推广计划的分层终止分析

    本文提出了一种新的方法，通过算法过程对广义计划的终止和可达性相关属性进行评估，并使用经验分析说明了该方法的范围和效果。

    Dec, 2022

  • 具有 Cut 操作的逻辑程序自动终止分析

    本文介绍了一种新的预处理方法，将 Prolog 程序自动转换为无割程序，进而证明定义逻辑程序的终止性，该方法已应用于终止证明器 AProVE 并取得成功。

    Jul, 2010

  • 检查逻辑程序使用函数符号的自下而上求值的终止性

    本篇论文研究了带有函数符号的逻辑程序在底部向上计算过程中的终止问题，并提出了 Gamma-acyclicity 和安全性等可判定的规则，同时阐述了这些规则在限制查询中的应用及程序的层次结构。

    Jul, 2014

  • 资源有限 ATL 生产与消耗模型检查的技术报告

    本文探讨考虑资源限制下的团体能力表达逻辑。前人已经研究了一些逻辑模型，这些模型仅考虑资源的消耗或系统中任何路径中生产或消耗资源的总量有界。本文针对生产和消耗资源无界的情形，研究了 RB-ATL 逻辑的模型检验问题，证明了问题是可判定的，但难度达到指数。同时，本文揭示了该问题的一些可处理情况，并对 RAL 资源逻辑的一种变体进行了详细比较，并提供了新的复杂性结果。

    Apr, 2015

  • 通过正定证明终止概率程序的分析

    针对非确定性概率程序的终止性质，提出了基于多项式守卫和分配的终止分析方法，通过 Positivstellensatz 的方法综合多项式级别超级马丁格斯来证明其终止性，并且还可以合成二次排名超级马丁格斯来处理复杂的程序。

    Apr, 2016