首页/论文/2001.01516

arXiv 2001.015162020-01cs.LOcs.PL

A Calculus for Modular Loop Acceleration

Florian Frohn

英文摘要：

Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs operating on integers. To this end, a variety of acceleration techniques has been proposed. However, all of them are monolithic: Either they accelerate a loop successfully or they fail completely. In contrast, we present a calculus that allows for combining acceleration techniques in a modular way and we show how to integrate many existing acceleration techniques into our calculus. Moreover, we propose two novel acceleration techniques that can be incorporated into our calculus seamlessly. An empirical evaluation demonstrates the applicability of our approach.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

A Calculus for Modular Loop Acceleration and Non-Termination Proofs

Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs. To this end, a variety of acceleration techniques has been proposed. However, so far all of them have been monolithic, i.e., a single loop could not be accelerated using a combination of several different acceleration techniques. In contrast, we present a calculus that allows for combining acceleration techniques in a modular way and we show how to integrate many existing acceleration techniques into our calculus. Moreover, we propose two novel acceleration techniques that can be inc…

2022-06-08cs.LOcs.PL

无限状态游戏中模块化吸引子加速（完整版本）

Modular Attractor Acceleration in Infinite-State Games (Full Version)

CISPA Helmholtz Center for Information Security（CISPA 赫尔姆霍兹信息安全中心）

本文提出模块化加速方法，通过组合简单论证提升无限状态游戏求解的效率和灵活性。

2026-01-20cs.LO

通过一阶转移系统实现高阶语言的模块化余归纳 up-to 技术

Modular coinduction up-to for higher-order languages via first-order transition systems

本文通过完全抽象翻译将一阶LTS上的up-to双模拟技术推广到高阶语言（π-演算、λ-演算及带引用的λ-演算），仅需手动验证新语言特有技术的相容性。

2021-09-16cs.LOcs.PL

ADCL：面向约束 Horn 子句的加速驱动子句学习

ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses

本文提出加速驱动子句学习（ADCL）演算，利用循环加速避免递归 CHCs 在归结证明中的重复推导，从而缩短证明，并在 LoAT 中实现后与现有工具实证比较。

2023-07-14cs.LO

Modular Construction of Fixed Point Combinators and Clocked Boehm Trees

Fixed point combinators (and their generalization: looping combinators) are classic notions belonging to the heart of lambda-calculus and logic. We start with an exploration of the structure of fixed point combinators (fpc's), vastly generalizing the well-known fact that if Y is an fpc, Y(SI) is again an fpc, generating the Boehm sequence of fpc's. Using the infinitary lambda-calculus we devise infinitely many other generation schemes for fpc's. In this way we find schemes and building blocks to construct new fpc's in a modular way. Having created a plethora of new fixed point combinators, the…

2010-02-12cs.LO

金融转移网络的Tuplix演算规范

Tuplix Calculus Specifications of Financial Transfer Networks

研究了Tuplix演算在模块化财务预算设计中的应用。我们使用财务转移网络来正式化组织结构。我们考虑了网络上货币流量的概念，以及一种方法来强制网络部分的流入和流出的匹配。我们利用所谓的有符号属性表示法，使内部流可见，通过命名。最后，我们提出了一个用于定义数据函数的Tuplix Calculus构造。

2008-05-13cs.CEcs.LO

更多相关论文收起更多论文

通过加速驱动子句学习证明非终止性（WST短篇版本）

Proving Non-Termination by Acceleration Driven Clause Learning (Short WST Version)

本研究将原本用于约束霍恩子句可满足性分析的加速驱动子句学习（ADCL）演算适配至转移系统非终止性证明场景，在工具LoAT中实现并与前沿方法开展对比评估。

2023-07-19cs.LO

A Time-Triggered Constraint-Based Calculus for Avionic Systems

The Integrated Modular Avionics (IMA) architec- ture and the Time-Triggered Ethernet (TTEthernet) network have emerged as the key components of a typical architecture model for recent civil aircrafts. We propose a real-time constraint-based calculus targeted at the analysis of such concepts of avionic embedded systems. We show our framework at work on the modelisation of both the (IMA) architecture and the TTEthernet network, illustrating their behavior by the well-known Flight Management System (FMS).

2014-10-12cs.LOcs.SE

通过加速驱动的子句学习证明非终止性

Proving Non-Termination by Acceleration Driven Clause Learning

本文将加速驱动子句学习（ADCL）适配到迁移系统，提出 ADCL-NT 变体用于证明程序非终止性，并在 LoAT 工具中实现和评估。

2023-07-07cs.LO

类型理论的模块化构造

A modular construction of type theories

本文提出理论U，一个模块化类型理论构造，使得多个逻辑系统的证明可表达，并证明子理论符号使用对应子理论证明。

2023-02-13cs.LOmath.LO

Factorize Factorization

Factorization -- a simple form of standardization -- is concerned with reduction strategies, i.e. how a result is computed. We present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which is inspired by the Hindley-Rosen technique for confluence. Specifically, our technique is well adapted to deal with extensions of the call-by-name and call-by-value lambda-calculi. The technique is first developed abstractly. We isolate a sufficient condition (called linear swap) for lifting factorization from components to the compound system, and which is…

2020-12-26cs.LO

Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)

We present the new version of the Loop Acceleration Tool (LoAT), a powerful tool for proving non-termination and worst-case lower bounds for programs operating on integers. It is based on a novel calculus for loop acceleration, i.e., transforming loops into non-deterministic straight-line code, and for finding non-terminating configurations. To implement it efficiently, LoAT uses a new approach based on SMT solving and unsat cores. An extensive evaluation shows that LoAT is highly competitive with other state-of-the-art tools for proving non-termination. While no other tool is able to deduce w…

2022-05-16cs.LO