On Quasi-Interpretations, Blind Abstractions and Implicit Complexity
准解释是一种保证一阶函数程序复杂性界限的技术：通过终止排序，它们给出了一个程序在多项式时间内可执行的充分条件，这里称为P-准则。为了更好地理解程序的内涵表达能力，我们研究了满足P-准则的程序的性质。给定一个二进制列表上的程序，它的盲抽象是通过将列表替换为它们的长度（自然数）而获得的不确定性程序。如果一个程序的盲抽象在多项式时间内终止，则该程序是盲多项式的。我们表明，所有的程序满足的P-准则的变种，实际上是盲目的多项式。然后，我们给出了两个扩展的P-准则：一个通过放松的终止序条件，和其他一个（有界值属性）给出了一个必要和充分条件的程序是多项式时间可执行的，与memoisation。
2006-08-06 cs.CC cs.LO cs.PL
Synthesis for Polynomial Lasso Programs
我们提出了一种方法的多项式套索程序的综合。这些程序由一个程序干、一组转换和一个退出条件组成，所有这些都以代数断言（多项式等式的合取）的形式出现。这种方法的核心是发现非线性（代数）循环不变量。我们扩展Sankaranarayanan，Sipma，和曼纳的基于模板的方法，并证明了一个完整的标准。我们执行程序合成通过生成一个约束，其解决方案是一个合成的程序与循环不变，证明程序的正确性。此约束是非线性的，并传递给SMT求解器。此外，我们可以强制终止的合成程序的测试用例的支持。
2013-11-16 cs.LO
Finding polynomial loop invariants for probabilistic programs
定量循环不变量是概率程序验证中的一个基本要素。最近，多元拉格朗日插值已被应用于综合多项式不变量。在本文中，我们提出了一种替代方法。首先，我们固定一个多项式模板作为循环不变量的候选。使用Stengle的Positivstellenetron和变换的平方和问题，我们找到了充分条件的系数。然后，我们解决了一个半定规划的可行性问题，综合循环不变量。如果半定规划不可行，则增加模板的度后进行回溯。我们的方法是半完全的，在这个意义上，它总是会导致我们一个可行的解决方案，如果一个存在和数值误差很小。实验结果表明了该方法的有效性。
2017-07-10 cs.LO
Tight Polynomial Bounds for Loop Programs in Polynomial Space
本文证明多项式空间中循环程序的紧多项式界问题是PSPACE完全的，并提出一种空间高效的分析算法，通过单变量界算法及几何归约实现多元界的计算。
2021-11-10 cs.LO
A programming language characterizing quantum polynomial time
本文提出一阶量子语言 FOQ 及其有界宽度子集 PFOQ，用以刻画量子复杂度类 FBQP，并给出将 PFOQ 程序编译为多项式规模量子电路的保持语义算法。
2025-10-20 cs.LO cs.PL
A generic imperative language for polynomial time
隐式计算复杂性中的派生方法与函数式编程有关，但考虑到命令式编程的更广泛的算法适用性，将其适用于通用命令式编程是非常可取的。我们介绍了一种新的方法，衍生，除其他好处外，很容易适应完全通用的命令式编程。新颖之处在于分歧有限的二阶对象，即有限的结构，而不是分歧自由代数的元素。在此过程中，我们在隐式复杂性的可行性类型论特征和静态分析的数据流方法之间架起了桥梁。
2020-02-19 cs.CC cs.LO cs.PL
Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
本文提出命令式程序LTL验证的可靠完备证据，并针对多项式算术程序给出自动合成LTL证据的高效算法，实验证明其能处理以往工具无法处理的程序。
2024-07-01 cs.LO cs.PL
Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization
虽然抽象解释在理论上并不局限于特定类型的属性，但在实践中，它主要用于计算可达集的线性过近似。程序的收集语义。用户提供的属性的验证不容易与通常的前向不动点计算使用数值抽象域兼容。我们建议在这里依靠平方和编程来表征属性驱动的多项式不变。这种不变量的生成可以由有界性来指导，或者相反，可以由要避免的状态空间的给定区域来指导。虽然目标属性不一定是归纳相对于程序语义，我们的方法确定了一个更强的归纳多项式不变量使用数值优化。我们的方法适用于广泛的程序集：一个主要的，而循环组成的析取（如果，然后，否则）的多项式更新，例如分段多项式控制器。它已在各种方案中得到评估。
2015-03-24 cs.LO
Polynomial Template Generation using Sum-of-Squares Programming
模板抽象域允许表达比经典抽象域更有趣的属性。然而，当使用模板抽象域进行程序分析时，模板生成是一个具有挑战性的问题。在本文中，我们与模板生成的程序属性，我们要证明。我们专注于嵌套条件分支的单循环程序。我们正式定义的概念，以及代表性的模板基础上，这样的程序和给定的属性。该定义依赖于模板抽象域产生归纳不变量的事实。我们表明，这些不变量可以通过解决某些系统的功能不等式。然后，这样的系统可以加强使用层次的平方和（SOS）的问题，当我们考虑程序编写的多项式算术。SOS层次结构的每一步都可能提供一个解决方案，该解决方案进而产生一个不变式以及所需属性持有的证书。这种方法的兴趣说明在多项式算术的非平凡的程序示例。
2014-10-18 cs.LO math.OC
Polynomial Invariants for Affine Programs
我们展示了一种算法来计算在给定仿射程序的每个位置处保持的最强多项式（或代数）不变量（即，只有非确定性（与条件相反）分支的程序，其所有赋值都由仿射表达式给出）。我们的主要工具是一个代数结果的独立利益：给定一组有限的理性方阵相同的尺寸，我们展示了如何计算Zebriki封闭的半群，他们产生。
2018-05-02 cs.DM cs.LO math.AG
Polytool: polynomial interpretations as a basis for termination analysis of Logic programs
我们的目标是研究移植终止分析技术开发的一个编程范式到另一个范式的可行性。在本文中，我们将展示如何适应终止分析技术的多项式解释的基础上-非常有名的术语重写系统（TRS）的背景下-获得新的（非转换）的终结分析技术，明确的逻辑程序（LP）。这导致了一种方法，可以被看作是一个直接推广的传统技术在终止分析的LP，线性规范和水平映射。我们的扩展一般化这些任意多项式。我们扩展了一些标准的概念和结果终止分析的上下文多项式的解释。我们还提出了一个基于约束的方法自动生成多项式的解释，满足终止条件。基于这种方法，我们实现了一个新的工具，称为Polytool，自动终止分析的LP。
2009-12-22 cs.LO cs.PL
Deciding Polynomial Termination Complexity for VASS Programs
我们表明，对于每一个固定的$k\geq 3$，一个给定的恶魔VASS的终止/计数器复杂度是否是$\mathcal{O}(n^k)$，$Ω(n^{k})$，和$Θ(n^{k})$的问题是NP完全，NP完全，DP完全，分别。我们还为$k\leq 2$对这些问题的复杂性进行了分类。这表明，多项式时间算法设计的强连接恶魔VASS在以前的作品不能扩展到一般情况下。然后，我们证明了VASS对策的相同问题是PSPACE完全的。同样，我们也对$k\leq 2$的复杂性进行了分类。有趣的是，易于处理的恶魔VASS和VASS游戏的子类，通过绑定某些结构参数，这开辟了道路，应用程序在程序分析，尽管提出了较低的复杂性界限。
2021-12-05 cs.LO
A Polynomial Translation of Logic Programs with Nested Expressions into Disjunctive Logic Programs: Preliminary Report
嵌套逻辑程序最近被引入，以便允许在答案集语义下的逻辑程序规则的头部和主体中的任意嵌套公式。嵌套表达式可以不受限制地使用合取、析取以及作为失败操作符的否定来形成。这为知识表示和推理提供了一个非常灵活和紧凑的框架。已有的结果表明，嵌套逻辑程序可以初等地转化为标准（非嵌套）析取逻辑程序，只需对体文字应用否定作为失败算子.这是非常实际的相关性，因为它允许我们评估嵌套的逻辑程序的手段，现成的析取逻辑编程系统，如DLV。然而，事实证明，这种简单的转换在最坏的情况下会导致指数爆破，尽管复杂性结果表明两种形式主义之间存在多项式转换。在本文中，我们接受了这一挑战，并提供了一个多项式的逻辑程序与嵌套表达式转换为析取逻辑程序。此外，我们表明，这种翻译是模块化的和（强）忠实。我们已经实现了简单的和高级的转换;生成的编译器作为DLV的前端，并在Web上公开提供。
2002-07-19 cs.AI cs.LO
Polynomial Invariant Generation for Non-deterministic Recursive Programs
我们考虑经典的问题，不变量生成的程序与多项式分配，并专注于合成不变量，是一个严格的多项式不等式的连接。我们提出了一个健全的和半完全的方法的基础上positivstellensaetze，即定理，在半代数几何的特点，正多项式在一个半代数集。据我们所知，这是第一个不变量生成方法，提供完整性保证的不变量组成的多项式不等式。此外，在理论方面，我们的方法的最坏情况的复杂性是次指数，而以前已知的完整的方法（Colon等，CAV 2003），它只能处理线性不变量的最坏情况的复杂性是指数。在实践方面，我们减少了不变量生成问题的二次规划（QCLP），这是一个经典的优化问题，许多工业求解器。最后，我们证明了我们的方法的适用性，通过提供实验结果在几个学术基准。
2020-04-06 cs.LO cs.PL
A Type-Based Complexity Analysis of Object Oriented Programs
介绍了一种面向对象的通用程序设计语言的类型系统，以推断资源上界。得到了多项式时间可计算函数集的一个可靠而完整的刻画。因此，类型化程序的堆空间和栈空间需求也是多项式有界的。这种类型系统的灵感来自于以前关于隐式计算复杂性的工作，使用分层和非干扰技术。所提出的方法有几个优点。首先，它为程序员提供了显式的大$O$多项式上界，因此它的使用可以允许程序员避免内存错误;其次，类型检查在多项式时间内是可判定的。最后，它具有良好的表达能力，因为它分析了大多数面向对象的特性，如继承，重载，重写和递归。此外，它可以处理由对象保护的循环，也可以扩展到改变控制流的语句，如break或return。
2018-02-19 cs.LO cs.PL
Positive Almost-Sure Termination of Polynomial Random Walks
本文针对概率程序终止性问题，证明步长随迭代多项式增长、分支概率恒定的多项式随机游走满足正几乎必然终止（PAST）的条件，并通过结合遗传规划等方法实现了相关阈值的近似。
2025-06-17 cs.LO
Flowchart Programs, Regular Expressions, and Decidability of Polynomial Growth-Rate
我们提出了一种新的方法来推断复杂性的性质，为一类程序的形式的流程图注释循环信息。具体来说，我们的方法可以（健全和完全）决定计算值是否作为输入的函数多项式有界;运行时间也是如此。这样的复杂性属性对于图灵完备程序设计语言来说是不可判定的，而在程序分析中，一个常见的解决方案是解决合理但不完整的解决方案。相比之下，我们认为一类程序是图灵不完全的，但足够强大，包括这种分析的几个挑战。对于一个具有良好结构语法的相关语言，类似于Meyer和Ritchie的LOOP程序，这个问题以前已经被证明是可判定的。分析依赖于程序的组合性，因此在获得类似的结果与任意控制流图的流程图程序的挑战。我们的挑战的答案是双重的：首先，我们提出了一类循环注释的流程图，这是更一般的流程图，直接代表结构化的程序;其次，我们提出了一种技术，重用的想法，从工作结构化的程序，并将它们应用到这样的流程图。该技术的灵感来自于非确定性自动机到正则表达式的经典翻译，但我们将构建这样一个表达式的指数成本降低，获得多项式时间分析。这些思想可以很好地适用于其他分析问题。
2016-07-08 cs.FL cs.LO cs.PL
A feasible and unitary quantum programming language
本文提出一种支持高阶程序与量子控制流的新型量子编程语言，通过叠加模态、正交性约束及基于线性逻辑和 Barber–Plotkin 对偶性的类型系统，同时保证酉性、多项式时间归一化与可行性。
2024-03-05 cs.LO cs.PL
On Learning Polynomial Recursive Programs
引入 P-finite automata 类，证明其可在 Angluin 的 MAT 模型中多项式时间精确学习，推广了 DFA 和加权自动机的经典可学习性结果。
2023-10-23 cs.FL cs.LO cs.PL
